Twierdzenie

start

Twierdzenie zawira słowo kluczowe theorem, formułę i uzasadnienie. Twierdzenie może być poprzedzone pragmatem? z nazwą.

::$N Kuratowski-Zorn Lemma
::$N Zorn Lemma
theorem :: ORDERS_1:65
  for X st X <> {} &
     for Z st Z c= X & Z is c=-linear
      ex Y st Y in X &
       for X1 st X1 in Z holds X1 c= Y
  ex Y st Y in X & for Z st Z in X & Z <> Y holds not Y c= Z;

Twierdzenie jest elementem eksportowalnym -- można powoływać się na nie w innych artykułach. Odwołanie dokonywane jest przez etykietę biblioteczną twierdzenia: <nazwa artykułu>:<kolejny numer>, np. NAT_1:13.