begin
:: deftheorem ORDERS_2:def 1 :
canceled;
:: deftheorem ORDERS_2:def 2 :
canceled;
:: deftheorem Def3 defines total ORDERS_2:def 3 :
:: deftheorem Def4 defines reflexive ORDERS_2:def 4 :
:: deftheorem Def5 defines transitive ORDERS_2:def 5 :
:: deftheorem Def6 defines antisymmetric ORDERS_2:def 6 :
Lm1:
for x being set
for A being non empty Poset
for S being Subset of st x in S holds
x is Element of
;
:: deftheorem ORDERS_2:def 7 :
canceled;
:: deftheorem ORDERS_2:def 8 :
canceled;
:: deftheorem Def9 defines <= ORDERS_2:def 9 :
:: deftheorem Def10 defines < ORDERS_2:def 10 :
for
A being
RelStr for
a1,
a2 being
Element of holds
(
a1 < a2 iff (
a1 <= a2 &
a1 <> a2 ) );
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th24:
theorem Th25:
theorem Th26:
theorem
canceled;
theorem Th28:
theorem Th29:
theorem Th30:
theorem
canceled;
theorem Th32:
:: deftheorem Def11 defines strongly_connected ORDERS_2:def 11 :
theorem
canceled;
theorem
canceled;
theorem Th35:
theorem Th36:
theorem
theorem Th38:
theorem Th39:
theorem Th40:
:: deftheorem defines UpperCone ORDERS_2:def 12 :
:: deftheorem defines LowerCone ORDERS_2:def 13 :
theorem
canceled;
theorem
canceled;
theorem Th43:
theorem
theorem
theorem
theorem Th47:
theorem
theorem Th49:
theorem Th50:
theorem
theorem Th52:
:: deftheorem defines InitSegm ORDERS_2:def 14 :
:: deftheorem Def15 defines Initial_Segm ORDERS_2:def 15 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th57:
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem Th62:
theorem
canceled;
theorem
theorem Th65:
theorem
canceled;
theorem Th67:
theorem Th68:
theorem Th69:
theorem Th70:
theorem Th71:
theorem
theorem Th73:
:: deftheorem Def16 defines Chain ORDERS_2:def 16 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th78:
theorem Th79:
theorem Th80:
theorem
theorem
theorem Th83:
theorem Th84:
:: deftheorem Def17 defines Chains ORDERS_2:def 17 :
Lm2:
for A being non empty Poset
for f being Choice_Function of BOOL the carrier of A holds union (Chains f) is Subset of
Lm3:
for A being non empty Poset
for f being Choice_Function of BOOL the carrier of A holds union (Chains f) is Chain of A
theorem
canceled;
theorem
canceled;
theorem Th87:
theorem Th88:
theorem Th89:
begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th107:
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem
Lm4:
for X, Y being set
for R being Relation st R is_connected_in X & Y c= X holds
R is_connected_in Y
Lm5:
for X, Y being set
for R being Relation st R well_orders X & Y c= X holds
R well_orders Y
theorem Th162:
theorem