:: ORDERS_1 semantic presentation

Lemma1: for b1 being set holds
( ex b2 being set st
( b2 <> {} & b2 in b1 ) iff union b1 <> {} )
proof end;

definition
let c1 be non empty set ;
assume E2: not {} in c1 ;
mode Choice_Function of c1 -> Function of a1, union a1 means :Def1: :: ORDERS_1:def 1
for b1 being set st b1 in a1 holds
a2 . b1 in b1;
existence
ex b1 being Function of c1, union c1 st
for b2 being set st b2 in c1 holds
b1 . b2 in b2
proof end;
end;

:: deftheorem Def1 defines Choice_Function ORDERS_1:def 1 :
for b1 being non empty set st not {} in b1 holds
for b2 being Function of b1, union b1 holds
( b2 is Choice_Function of b1 iff for b3 being set st b3 in b1 holds
b2 . b3 in b3 );

definition
let c1 be set ;
func BOOL c1 -> set equals :: ORDERS_1:def 2
(bool a1) \ {{} };
coherence
(bool c1) \ {{} } is set ;
end;

:: deftheorem Def2 defines BOOL ORDERS_1:def 2 :
for b1 being set holds BOOL b1 = (bool b1) \ {{} };

registration
let c1 be non empty set ;
cluster BOOL a1 -> non empty ;
coherence
not BOOL c1 is empty
proof end;
end;

theorem Th1: :: ORDERS_1:1
canceled;

theorem Th2: :: ORDERS_1:2
canceled;

theorem Th3: :: ORDERS_1:3
canceled;

theorem Th4: :: ORDERS_1:4
for b1 being non empty set holds not {} in BOOL b1
proof end;

theorem Th5: :: ORDERS_1:5
for b1, b2 being non empty set holds
( b1 c= b2 iff b1 in BOOL b2 )
proof end;

theorem Th6: :: ORDERS_1:6
for b1, b2 being non empty set holds
( b1 is Subset of b2 iff b1 in BOOL b2 ) by Th5;

theorem Th7: :: ORDERS_1:7
for b1 being non empty set holds b1 in BOOL b1 by Th5;

definition
let c1 be set ;
mode Order of a1 is reflexive antisymmetric transitive total Relation of a1;
end;

Lemma4: for b1 being set
for b2 being total Relation of b1 holds field b2 = b1
proof end;

theorem Th8: :: ORDERS_1:8
canceled;

theorem Th9: :: ORDERS_1:9
canceled;

theorem Th10: :: ORDERS_1:10
canceled;

theorem Th11: :: ORDERS_1:11
canceled;

theorem Th12: :: ORDERS_1:12
for b1, b2 being set
for b3 being Order of b1 st b2 in b1 holds
[b2,b2] in b3
proof end;

theorem Th13: :: ORDERS_1:13
for b1, b2, b3 being set
for b4 being Order of b1 st b2 in b1 & b3 in b1 & [b2,b3] in b4 & [b3,b2] in b4 holds
b2 = b3
proof end;

theorem Th14: :: ORDERS_1:14
for b1, b2, b3, b4 being set
for b5 being Order of b1 st b2 in b1 & b3 in b1 & b4 in b1 & [b2,b3] in b5 & [b3,b4] in b5 holds
[b2,b4] in b5
proof end;

theorem Th15: :: ORDERS_1:15
canceled;

theorem Th16: :: ORDERS_1:16
canceled;

theorem Th17: :: ORDERS_1:17
canceled;

theorem Th18: :: ORDERS_1:18
canceled;

theorem Th19: :: ORDERS_1:19
canceled;

theorem Th20: :: ORDERS_1:20
canceled;

theorem Th21: :: ORDERS_1:21
canceled;

theorem Th22: :: ORDERS_1:22
canceled;

theorem Th23: :: ORDERS_1:23
canceled;

theorem Th24: :: ORDERS_1:24
canceled;

theorem Th25: :: ORDERS_1:25
canceled;

theorem Th26: :: ORDERS_1:26
canceled;

theorem Th27: :: ORDERS_1:27
canceled;

theorem Th28: :: ORDERS_1:28
canceled;

theorem Th29: :: ORDERS_1:29
canceled;

theorem Th30: :: ORDERS_1:30
canceled;

theorem Th31: :: ORDERS_1:31
canceled;

theorem Th32: :: ORDERS_1:32
canceled;

theorem Th33: :: ORDERS_1:33
canceled;

theorem Th34: :: ORDERS_1:34
canceled;

theorem Th35: :: ORDERS_1:35
canceled;

theorem Th36: :: ORDERS_1:36
canceled;

theorem Th37: :: ORDERS_1:37
canceled;

theorem Th38: :: ORDERS_1:38
canceled;

theorem Th39: :: ORDERS_1:39
canceled;

theorem Th40: :: ORDERS_1:40
canceled;

theorem Th41: :: ORDERS_1:41
canceled;

theorem Th42: :: ORDERS_1:42
canceled;

theorem Th43: :: ORDERS_1:43
canceled;

theorem Th44: :: ORDERS_1:44
canceled;

theorem Th45: :: ORDERS_1:45
canceled;

theorem Th46: :: ORDERS_1:46
canceled;

theorem Th47: :: ORDERS_1:47
canceled;

theorem Th48: :: ORDERS_1:48
canceled;

theorem Th49: :: ORDERS_1:49
canceled;

theorem Th50: :: ORDERS_1:50
canceled;

theorem Th51: :: ORDERS_1:51
canceled;

theorem Th52: :: ORDERS_1:52
canceled;

theorem Th53: :: ORDERS_1:53
canceled;

theorem Th54: :: ORDERS_1:54
canceled;

theorem Th55: :: ORDERS_1:55
canceled;

theorem Th56: :: ORDERS_1:56
canceled;

theorem Th57: :: ORDERS_1:57
canceled;

theorem Th58: :: ORDERS_1:58
canceled;

theorem Th59: :: ORDERS_1:59
canceled;

theorem Th60: :: ORDERS_1:60
canceled;

theorem Th61: :: ORDERS_1:61
canceled;

theorem Th62: :: ORDERS_1:62
canceled;

theorem Th63: :: ORDERS_1:63
canceled;

theorem Th64: :: ORDERS_1:64
canceled;

theorem Th65: :: ORDERS_1:65
canceled;

theorem Th66: :: ORDERS_1:66
canceled;

theorem Th67: :: ORDERS_1:67
canceled;

theorem Th68: :: ORDERS_1:68
canceled;

theorem Th69: :: ORDERS_1:69
canceled;

theorem Th70: :: ORDERS_1:70
canceled;

theorem Th71: :: ORDERS_1:71
canceled;

theorem Th72: :: ORDERS_1:72
canceled;

theorem Th73: :: ORDERS_1:73
canceled;

theorem Th74: :: ORDERS_1:74
canceled;

theorem Th75: :: ORDERS_1:75
canceled;

theorem Th76: :: ORDERS_1:76
canceled;

theorem Th77: :: ORDERS_1:77
canceled;

theorem Th78: :: ORDERS_1:78
canceled;

theorem Th79: :: ORDERS_1:79
canceled;

theorem Th80: :: ORDERS_1:80
canceled;

theorem Th81: :: ORDERS_1:81
canceled;

theorem Th82: :: ORDERS_1:82
canceled;

theorem Th83: :: ORDERS_1:83
canceled;

theorem Th84: :: ORDERS_1:84
canceled;

theorem Th85: :: ORDERS_1:85
canceled;

theorem Th86: :: ORDERS_1:86
canceled;

theorem Th87: :: ORDERS_1:87
canceled;

theorem Th88: :: ORDERS_1:88
canceled;

theorem Th89: :: ORDERS_1:89
canceled;

theorem Th90: :: ORDERS_1:90
canceled;

theorem Th91: :: ORDERS_1:91
for b1 being set holds
( ex b2 being set st
( b2 <> {} & b2 in b1 ) iff union b1 <> {} ) by Lemma1;

theorem Th92: :: ORDERS_1:92
for b1 being set
for b2 being Relation holds
( b2 is_strongly_connected_in b1 iff ( b2 is_reflexive_in b1 & b2 is_connected_in b1 ) )
proof end;

theorem Th93: :: ORDERS_1:93
for b1, b2 being set
for b3 being Relation st b3 is_reflexive_in b1 & b2 c= b1 holds
b3 is_reflexive_in b2
proof end;

theorem Th94: :: ORDERS_1:94
for b1, b2 being set
for b3 being Relation st b3 is_antisymmetric_in b1 & b2 c= b1 holds
b3 is_antisymmetric_in b2
proof end;

theorem Th95: :: ORDERS_1:95
for b1, b2 being set
for b3 being Relation st b3 is_transitive_in b1 & b2 c= b1 holds
b3 is_transitive_in b2
proof end;

theorem Th96: :: ORDERS_1:96
for b1, b2 being set
for b3 being Relation st b3 is_strongly_connected_in b1 & b2 c= b1 holds
b3 is_strongly_connected_in b2
proof end;

theorem Th97: :: ORDERS_1:97
for b1 being set
for b2 being total Relation of b1 holds field b2 = b1 by Lemma4;

theorem Th98: :: ORDERS_1:98
for b1 being set
for b2 being Relation of b1 st b2 is_reflexive_in b1 holds
( dom b2 = b1 & field b2 = b1 )
proof end;

theorem Th99: :: ORDERS_1:99
for b1 being set
for b2 being Order of b1 holds
( dom b2 = b1 & rng b2 = b1 )
proof end;

theorem Th100: :: ORDERS_1:100
for b1 being set
for b2 being Order of b1 holds field b2 = b1
proof end;

definition
let c1 be Relation;
attr a1 is being_quasi-order means :: ORDERS_1:def 3
( a1 is reflexive & a1 is transitive );
attr a1 is being_partial-order means :Def4: :: ORDERS_1:def 4
( a1 is reflexive & a1 is transitive & a1 is antisymmetric );
attr a1 is being_linear-order means :Def5: :: ORDERS_1:def 5
( a1 is reflexive & a1 is transitive & a1 is antisymmetric & a1 is connected );
end;

:: deftheorem Def3 defines being_quasi-order ORDERS_1:def 3 :
for b1 being Relation holds
( b1 is being_quasi-order iff ( b1 is reflexive & b1 is transitive ) );

:: deftheorem Def4 defines being_partial-order ORDERS_1:def 4 :
for b1 being Relation holds
( b1 is being_partial-order iff ( b1 is reflexive & b1 is transitive & b1 is antisymmetric ) );

:: deftheorem Def5 defines being_linear-order ORDERS_1:def 5 :
for b1 being Relation holds
( b1 is being_linear-order iff ( b1 is reflexive & b1 is transitive & b1 is antisymmetric & b1 is connected ) );

notation
let c1 be Relation;
synonym c1 is_quasi-order for being_quasi-order c1;
synonym c1 is_partial-order for being_partial-order c1;
synonym c1 is_linear-order for being_linear-order c1;
end;

theorem Th101: :: ORDERS_1:101
canceled;

theorem Th102: :: ORDERS_1:102
canceled;

theorem Th103: :: ORDERS_1:103
canceled;

theorem Th104: :: ORDERS_1:104
for b1 being Relation st b1 is_quasi-order holds
b1 ~ is_quasi-order
proof end;

theorem Th105: :: ORDERS_1:105
for b1 being Relation st b1 is_partial-order holds
b1 ~ is_partial-order
proof end;

Lemma14: for b1 being Relation st b1 is connected holds
b1 ~ is connected
proof end;

theorem Th106: :: ORDERS_1:106
for b1 being Relation st b1 is_linear-order holds
b1 ~ is_linear-order
proof end;

theorem Th107: :: ORDERS_1:107
for b1 being Relation st b1 is well-ordering holds
( b1 is_quasi-order & b1 is_partial-order & b1 is_linear-order )
proof end;

theorem Th108: :: ORDERS_1:108
for b1 being Relation st b1 is_linear-order holds
( b1 is_quasi-order & b1 is_partial-order )
proof end;

theorem Th109: :: ORDERS_1:109
for b1 being Relation st b1 is_partial-order holds
b1 is_quasi-order
proof end;

theorem Th110: :: ORDERS_1:110
for b1 being set
for b2 being Order of b1 holds b2 is_partial-order by Def4;

theorem Th111: :: ORDERS_1:111
for b1 being set
for b2 being Order of b1 holds b2 is_quasi-order
proof end;

theorem Th112: :: ORDERS_1:112
for b1 being set
for b2 being Order of b1 st b2 is connected holds
b2 is_linear-order by Def5;

Lemma17: for b1 being Relation holds b1 c= [:(field b1),(field b1):]
proof end;

Lemma18: for b1 being Relation
for b2 being set st b1 is reflexive & b2 c= field b1 holds
field (b1 |_2 b2) = b2
proof end;

theorem Th113: :: ORDERS_1:113
for b1 being Relation
for b2 being set st b1 is_quasi-order holds
b1 |_2 b2 is_quasi-order
proof end;

theorem Th114: :: ORDERS_1:114
for b1 being Relation
for b2 being set st b1 is_partial-order holds
b1 |_2 b2 is_partial-order
proof end;

theorem Th115: :: ORDERS_1:115
for b1 being Relation
for b2 being set st b1 is_linear-order holds
b1 |_2 b2 is_linear-order
proof end;

theorem Th116: :: ORDERS_1:116
canceled;

theorem Th117: :: ORDERS_1:117
canceled;

theorem Th118: :: ORDERS_1:118
canceled;

theorem Th119: :: ORDERS_1:119
( {} is_quasi-order & {} is_partial-order & {} is_linear-order & {} is well-ordering )
proof end;

theorem Th120: :: ORDERS_1:120
for b1 being set holds
( id b1 is_quasi-order & id b1 is_partial-order )
proof end;

definition
let c1 be Relation;
let c2 be set ;
pred c1 quasi_orders c2 means :Def6: :: ORDERS_1:def 6
( a1 is_reflexive_in a2 & a1 is_transitive_in a2 );
pred c1 partially_orders c2 means :Def7: :: ORDERS_1:def 7
( a1 is_reflexive_in a2 & a1 is_transitive_in a2 & a1 is_antisymmetric_in a2 );
pred c1 linearly_orders c2 means :: ORDERS_1:def 8
( a1 is_reflexive_in a2 & a1 is_transitive_in a2 & a1 is_antisymmetric_in a2 & a1 is_connected_in a2 );
end;

:: deftheorem Def6 defines quasi_orders ORDERS_1:def 6 :
for b1 being Relation
for b2 being set holds
( b1 quasi_orders b2 iff ( b1 is_reflexive_in b2 & b1 is_transitive_in b2 ) );

:: deftheorem Def7 defines partially_orders ORDERS_1:def 7 :
for b1 being Relation
for b2 being set holds
( b1 partially_orders b2 iff ( b1 is_reflexive_in b2 & b1 is_transitive_in b2 & b1 is_antisymmetric_in b2 ) );

:: deftheorem Def8 defines linearly_orders ORDERS_1:def 8 :
for b1 being Relation
for b2 being set holds
( b1 linearly_orders b2 iff ( b1 is_reflexive_in b2 & b1 is_transitive_in b2 & b1 is_antisymmetric_in b2 & b1 is_connected_in b2 ) );

theorem Th121: :: ORDERS_1:121
canceled;

theorem Th122: :: ORDERS_1:122
canceled;

theorem Th123: :: ORDERS_1:123
canceled;

theorem Th124: :: ORDERS_1:124
for b1 being Relation
for b2 being set st b1 well_orders b2 holds
( b1 quasi_orders b2 & b1 partially_orders b2 & b1 linearly_orders b2 )
proof end;

theorem Th125: :: ORDERS_1:125
for b1 being Relation
for b2 being set st b1 linearly_orders b2 holds
( b1 quasi_orders b2 & b1 partially_orders b2 )
proof end;

theorem Th126: :: ORDERS_1:126
for b1 being Relation
for b2 being set st b1 partially_orders b2 holds
b1 quasi_orders b2
proof end;

theorem Th127: :: ORDERS_1:127
for b1 being Relation st b1 is_quasi-order holds
b1 quasi_orders field b1
proof end;

theorem Th128: :: ORDERS_1:128
for b1 being Relation
for b2, b3 being set st b1 quasi_orders b2 & b3 c= b2 holds
b1 quasi_orders b3
proof end;

Lemma26: for b1 being Relation
for b2 being set st b1 is_reflexive_in b2 holds
b1 |_2 b2 is reflexive
proof end;

Lemma27: for b1 being Relation
for b2 being set st b1 is_transitive_in b2 holds
b1 |_2 b2 is transitive
proof end;

Lemma28: for b1 being Relation
for b2 being set st b1 is_antisymmetric_in b2 holds
b1 |_2 b2 is antisymmetric
proof end;

Lemma29: for b1 being Relation
for b2 being set st b1 is_connected_in b2 holds
b1 |_2 b2 is connected
proof end;

theorem Th129: :: ORDERS_1:129
for b1 being Relation
for b2 being set st b1 quasi_orders b2 holds
b1 |_2 b2 is_quasi-order
proof end;

theorem Th130: :: ORDERS_1:130
for b1 being Relation st b1 is_partial-order holds
b1 partially_orders field b1
proof end;

theorem Th131: :: ORDERS_1:131
for b1 being Relation
for b2, b3 being set st b1 partially_orders b2 & b3 c= b2 holds
b1 partially_orders b3
proof end;

theorem Th132: :: ORDERS_1:132
for b1 being Relation
for b2 being set st b1 partially_orders b2 holds
b1 |_2 b2 is_partial-order
proof end;

Lemma31: for b1 being Relation
for b2, b3 being set st b1 is_connected_in b2 & b3 c= b2 holds
b1 is_connected_in b3
proof end;

theorem Th133: :: ORDERS_1:133
for b1 being Relation st b1 is_linear-order holds
b1 linearly_orders field b1
proof end;

theorem Th134: :: ORDERS_1:134
for b1 being Relation
for b2, b3 being set st b1 linearly_orders b2 & b3 c= b2 holds
b1 linearly_orders b3
proof end;

theorem Th135: :: ORDERS_1:135
for b1 being Relation
for b2 being set st b1 linearly_orders b2 holds
b1 |_2 b2 is_linear-order
proof end;

Lemma32: for b1 being Relation
for b2 being set st b1 is_reflexive_in b2 holds
b1 ~ is_reflexive_in b2
proof end;

Lemma33: for b1 being Relation
for b2 being set st b1 is_transitive_in b2 holds
b1 ~ is_transitive_in b2
proof end;

Lemma34: for b1 being Relation
for b2 being set st b1 is_antisymmetric_in b2 holds
b1 ~ is_antisymmetric_in b2
proof end;

Lemma35: for b1 being Relation
for b2 being set st b1 is_connected_in b2 holds
b1 ~ is_connected_in b2
proof end;

theorem Th136: :: ORDERS_1:136
for b1 being Relation
for b2 being set st b1 quasi_orders b2 holds
b1 ~ quasi_orders b2
proof end;

theorem Th137: :: ORDERS_1:137
for b1 being Relation
for b2 being set st b1 partially_orders b2 holds
b1 ~ partially_orders b2
proof end;

theorem Th138: :: ORDERS_1:138
for b1 being Relation
for b2 being set st b1 linearly_orders b2 holds
b1 ~ linearly_orders b2
proof end;

theorem Th139: :: ORDERS_1:139
for b1 being set
for b2 being Order of b1 holds b2 quasi_orders b1
proof end;

theorem Th140: :: ORDERS_1:140
for b1 being set
for b2 being Order of b1 holds b2 partially_orders b1
proof end;

theorem Th141: :: ORDERS_1:141
for b1 being Relation
for b2 being set st b1 partially_orders b2 holds
b1 |_2 b2 is Order of b2
proof end;

theorem Th142: :: ORDERS_1:142
for b1 being Relation
for b2 being set st b1 linearly_orders b2 holds
b1 |_2 b2 is Order of b2
proof end;

theorem Th143: :: ORDERS_1:143
for b1 being Relation
for b2 being set st b1 well_orders b2 holds
b1 |_2 b2 is Order of b2
proof end;

theorem Th144: :: ORDERS_1:144
canceled;

theorem Th145: :: ORDERS_1:145
canceled;

theorem Th146: :: ORDERS_1:146
for b1 being set holds
( id b1 quasi_orders b1 & id b1 partially_orders b1 )
proof end;

definition
let c1 be Relation;
let c2 be set ;
pred c2 has_upper_Zorn_property_wrt c1 means :Def9: :: ORDERS_1:def 9
for b1 being set st b1 c= a2 & a1 |_2 b1 is_linear-order holds
ex b2 being set st
( b2 in a2 & ( for b3 being set st b3 in b1 holds
[b3,b2] in a1 ) );
pred c2 has_lower_Zorn_property_wrt c1 means :: ORDERS_1:def 10
for b1 being set st b1 c= a2 & a1 |_2 b1 is_linear-order holds
ex b2 being set st
( b2 in a2 & ( for b3 being set st b3 in b1 holds
[b2,b3] in a1 ) );
end;

:: deftheorem Def9 defines has_upper_Zorn_property_wrt ORDERS_1:def 9 :
for b1 being Relation
for b2 being set holds
( b2 has_upper_Zorn_property_wrt b1 iff for b3 being set st b3 c= b2 & b1 |_2 b3 is_linear-order holds
ex b4 being set st
( b4 in b2 & ( for b5 being set st b5 in b3 holds
[b5,b4] in b1 ) ) );

:: deftheorem Def10 defines has_lower_Zorn_property_wrt ORDERS_1:def 10 :
for b1 being Relation
for b2 being set holds
( b2 has_lower_Zorn_property_wrt b1 iff for b3 being set st b3 c= b2 & b1 |_2 b3 is_linear-order holds
ex b4 being set st
( b4 in b2 & ( for b5 being set st b5 in b3 holds
[b4,b5] in b1 ) ) );

Lemma39: for b1 being Relation
for b2 being set holds (b1 |_2 b2) ~ = (b1 ~ ) |_2 b2
proof end;

E40: now
let c1 be Relation;
thus c1 |_2 {} = ({} | c1) | {} by WELLORD1:17
.= {} by RELAT_1:110 ;
end;

theorem Th147: :: ORDERS_1:147
canceled;

theorem Th148: :: ORDERS_1:148
canceled;

theorem Th149: :: ORDERS_1:149
for b1 being Relation
for b2 being set st b2 has_upper_Zorn_property_wrt b1 holds
b2 <> {}
proof end;

theorem Th150: :: ORDERS_1:150
for b1 being Relation
for b2 being set st b2 has_lower_Zorn_property_wrt b1 holds
b2 <> {}
proof end;

theorem Th151: :: ORDERS_1:151
for b1 being Relation
for b2 being set holds
( b2 has_upper_Zorn_property_wrt b1 iff b2 has_lower_Zorn_property_wrt b1 ~ )
proof end;

theorem Th152: :: ORDERS_1:152
for b1 being Relation
for b2 being set holds
( b2 has_upper_Zorn_property_wrt b1 ~ iff b2 has_lower_Zorn_property_wrt b1 )
proof end;

definition
let c1 be Relation;
let c2 be set ;
pred c2 is_maximal_in c1 means :Def11: :: ORDERS_1:def 11
( a2 in field a1 & ( for b1 being set holds
( not b1 in field a1 or not b1 <> a2 or not [a2,b1] in a1 ) ) );
pred c2 is_minimal_in c1 means :Def12: :: ORDERS_1:def 12
( a2 in field a1 & ( for b1 being set holds
( not b1 in field a1 or not b1 <> a2 or not [b1,a2] in a1 ) ) );
pred c2 is_superior_of c1 means :Def13: :: ORDERS_1:def 13
( a2 in field a1 & ( for b1 being set st b1 in field a1 & b1 <> a2 holds
[b1,a2] in a1 ) );
pred c2 is_inferior_of c1 means :Def14: :: ORDERS_1:def 14
( a2 in field a1 & ( for b1 being set st b1 in field a1 & b1 <> a2 holds
[a2,b1] in a1 ) );
end;

:: deftheorem Def11 defines is_maximal_in ORDERS_1:def 11 :
for b1 being Relation
for b2 being set holds
( b2 is_maximal_in b1 iff ( b2 in field b1 & ( for b3 being set holds
( not b3 in field b1 or not b3 <> b2 or not [b2,b3] in b1 ) ) ) );

:: deftheorem Def12 defines is_minimal_in ORDERS_1:def 12 :
for b1 being Relation
for b2 being set holds
( b2 is_minimal_in b1 iff ( b2 in field b1 & ( for b3 being set holds
( not b3 in field b1 or not b3 <> b2 or not [b3,b2] in b1 ) ) ) );

:: deftheorem Def13 defines is_superior_of ORDERS_1:def 13 :
for b1 being Relation
for b2 being set holds
( b2 is_superior_of b1 iff ( b2 in field b1 & ( for b3 being set st b3 in field b1 & b3 <> b2 holds
[b3,b2] in b1 ) ) );

:: deftheorem Def14 defines is_inferior_of ORDERS_1:def 14 :
for b1 being Relation
for b2 being set holds
( b2 is_inferior_of b1 iff ( b2 in field b1 & ( for b3 being set st b3 in field b1 & b3 <> b2 holds
[b2,b3] in b1 ) ) );

theorem Th153: :: ORDERS_1:153
canceled;

theorem Th154: :: ORDERS_1:154
canceled;

theorem Th155: :: ORDERS_1:155
canceled;

theorem Th156: :: ORDERS_1:156
canceled;

theorem Th157: :: ORDERS_1:157
for b1 being Relation
for b2 being set st b2 is_inferior_of b1 & b1 is antisymmetric holds
b2 is_minimal_in b1
proof end;

theorem Th158: :: ORDERS_1:158
for b1 being Relation
for b2 being set st b2 is_superior_of b1 & b1 is antisymmetric holds
b2 is_maximal_in b1
proof end;

theorem Th159: :: ORDERS_1:159
for b1 being Relation
for b2 being set st b2 is_minimal_in b1 & b1 is connected holds
b2 is_inferior_of b1
proof end;

theorem Th160: :: ORDERS_1:160
for b1 being Relation
for b2 being set st b2 is_maximal_in b1 & b1 is connected holds
b2 is_superior_of b1
proof end;

theorem Th161: :: ORDERS_1:161
for b1 being Relation
for b2, b3 being set st b2 in b3 & b2 is_superior_of b1 & b3 c= field b1 & b1 is reflexive holds
b3 has_upper_Zorn_property_wrt b1
proof end;

theorem Th162: :: ORDERS_1:162
for b1 being Relation
for b2, b3 being set st b2 in b3 & b2 is_inferior_of b1 & b3 c= field b1 & b1 is reflexive holds
b3 has_lower_Zorn_property_wrt b1
proof end;

theorem Th163: :: ORDERS_1:163
for b1 being Relation
for b2 being set holds
( b2 is_minimal_in b1 iff b2 is_maximal_in b1 ~ )
proof end;

theorem Th164: :: ORDERS_1:164
for b1 being Relation
for b2 being set holds
( b2 is_minimal_in b1 ~ iff b2 is_maximal_in b1 )
proof end;

theorem Th165: :: ORDERS_1:165
for b1 being Relation
for b2 being set holds
( b2 is_inferior_of b1 iff b2 is_superior_of b1 ~ )
proof end;

theorem Th166: :: ORDERS_1:166
for b1 being Relation
for b2 being set holds
( b2 is_inferior_of b1 ~ iff b2 is_superior_of b1 )
proof end;

Lemma48: for b1 being Relation
for b2, b3 being set st b1 well_orders b2 & b3 c= b2 holds
b1 well_orders b3
proof end;

theorem Th167: :: ORDERS_1:167
canceled;

theorem Th168: :: ORDERS_1:168
canceled;

theorem Th169: :: ORDERS_1:169
canceled;

theorem Th170: :: ORDERS_1:170
canceled;

theorem Th171: :: ORDERS_1:171
canceled;

theorem Th172: :: ORDERS_1:172
canceled;

theorem Th173: :: ORDERS_1:173
for b1 being Relation
for b2 being set st b1 partially_orders b2 & field b1 = b2 & b2 has_upper_Zorn_property_wrt b1 holds
ex b3 being set st b3 is_maximal_in b1
proof end;

theorem Th174: :: ORDERS_1:174
for b1 being Relation
for b2 being set st b1 partially_orders b2 & field b1 = b2 & b2 has_lower_Zorn_property_wrt b1 holds
ex b3 being set st b3 is_minimal_in b1
proof end;

theorem Th175: :: ORDERS_1:175
for b1 being set st b1 <> {} & ( for b2 being set st b2 c= b1 & b2 is c=-linear holds
ex b3 being set st
( b3 in b1 & ( for b4 being set st b4 in b2 holds
b4 c= b3 ) ) ) holds
ex b2 being set st
( b2 in b1 & ( for b3 being set st b3 in b1 & b3 <> b2 holds
not b2 c= b3 ) )
proof end;

theorem Th176: :: ORDERS_1:176
for b1 being set st b1 <> {} & ( for b2 being set st b2 c= b1 & b2 is c=-linear holds
ex b3 being set st
( b3 in b1 & ( for b4 being set st b4 in b2 holds
b3 c= b4 ) ) ) holds
ex b2 being set st
( b2 in b1 & ( for b3 being set st b3 in b1 & b3 <> b2 holds
not b3 c= b2 ) )
proof end;

theorem Th177: :: ORDERS_1:177
for b1 being set st b1 <> {} & ( for b2 being set st b2 <> {} & b2 c= b1 & b2 is c=-linear holds
union b2 in b1 ) holds
ex b2 being set st
( b2 in b1 & ( for b3 being set st b3 in b1 & b3 <> b2 holds
not b2 c= b3 ) )
proof end;

theorem Th178: :: ORDERS_1:178
for b1 being set st b1 <> {} & ( for b2 being set st b2 <> {} & b2 c= b1 & b2 is c=-linear holds
meet b2 in b1 ) holds
ex b2 being set st
( b2 in b1 & ( for b3 being set st b3 in b1 & b3 <> b2 holds
not b3 c= b2 ) )
proof end;

scheme :: ORDERS_1:sch 1
s1{ F1() -> non empty set , P1[ set , set ] } :
ex b1 being Element of F1() st
for b2 being Element of F1() st b1 <> b2 holds
not P1[b1,b2]
provided
E54: for b1 being Element of F1() holds P1[b1,b1] and
E55: for b1, b2 being Element of F1() st P1[b1,b2] & P1[b2,b1] holds
b1 = b2 and
E56: for b1, b2, b3 being Element of F1() st P1[b1,b2] & P1[b2,b3] holds
P1[b1,b3] and
E57: for b1 being set st b1 c= F1() & ( for b2, b3 being Element of F1() st b2 in b1 & b3 in b1 & P1[b2,b3] holds
P1[b3,b2] ) holds
ex b2 being Element of F1() st
for b3 being Element of F1() st b3 in b1 holds
P1[b3,b2]
proof end;

scheme :: ORDERS_1:sch 2
s2{ F1() -> non empty set , P1[ set , set ] } :
ex b1 being Element of F1() st
for b2 being Element of F1() st b1 <> b2 holds
not P1[b2,b1]
provided
E54: for b1 being Element of F1() holds P1[b1,b1] and
E55: for b1, b2 being Element of F1() st P1[b1,b2] & P1[b2,b1] holds
b1 = b2 and
E56: for b1, b2, b3 being Element of F1() st P1[b1,b2] & P1[b2,b3] holds
P1[b1,b3] and
E57: for b1 being set st b1 c= F1() & ( for b2, b3 being Element of F1() st b2 in b1 & b3 in b1 & P1[b2,b3] holds
P1[b3,b2] ) holds
ex b2 being Element of F1() st
for b3 being Element of F1() st b3 in b1 holds
P1[b2,b3]
proof end;

theorem Th179: :: ORDERS_1:179
for b1 being Relation
for b2 being set st b1 partially_orders b2 & field b1 = b2 holds
ex b3 being Relation st
( b1 c= b3 & b3 linearly_orders b2 & field b3 = b2 )
proof end;

theorem Th180: :: ORDERS_1:180
for b1 being Relation holds b1 c= [:(field b1),(field b1):] by Lemma17;

theorem Th181: :: ORDERS_1:181
for b1 being Relation
for b2 being set st b1 is reflexive & b2 c= field b1 holds
field (b1 |_2 b2) = b2 by Lemma18;

theorem Th182: :: ORDERS_1:182
for b1 being Relation
for b2 being set st b1 is_reflexive_in b2 holds
b1 |_2 b2 is reflexive by Lemma26;

theorem Th183: :: ORDERS_1:183
for b1 being Relation
for b2 being set st b1 is_transitive_in b2 holds
b1 |_2 b2 is transitive by Lemma27;

theorem Th184: :: ORDERS_1:184
for b1 being Relation
for b2 being set st b1 is_antisymmetric_in b2 holds
b1 |_2 b2 is antisymmetric by Lemma28;

theorem Th185: :: ORDERS_1:185
for b1 being Relation
for b2 being set st b1 is_connected_in b2 holds
b1 |_2 b2 is connected by Lemma29;

theorem Th186: :: ORDERS_1:186
for b1 being Relation
for b2, b3 being set st b1 is_connected_in b2 & b3 c= b2 holds
b1 is_connected_in b3 by Lemma31;

theorem Th187: :: ORDERS_1:187
for b1 being Relation
for b2, b3 being set st b1 well_orders b2 & b3 c= b2 holds
b1 well_orders b3 by Lemma48;

theorem Th188: :: ORDERS_1:188
for b1 being Relation st b1 is connected holds
b1 ~ is connected by Lemma14;

theorem Th189: :: ORDERS_1:189
for b1 being Relation
for b2 being set st b1 is_reflexive_in b2 holds
b1 ~ is_reflexive_in b2 by Lemma32;

theorem Th190: :: ORDERS_1:190
for b1 being Relation
for b2 being set st b1 is_transitive_in b2 holds
b1 ~ is_transitive_in b2 by Lemma33;

theorem Th191: :: ORDERS_1:191
for b1 being Relation
for b2 being set st b1 is_antisymmetric_in b2 holds
b1 ~ is_antisymmetric_in b2 by Lemma34;

theorem Th192: :: ORDERS_1:192
for b1 being Relation
for b2 being set st b1 is_connected_in b2 holds
b1 ~ is_connected_in b2 by Lemma35;

theorem Th193: :: ORDERS_1:193
for b1 being Relation
for b2 being set holds (b1 |_2 b2) ~ = (b1 ~ ) |_2 b2 by Lemma39;

theorem Th194: :: ORDERS_1:194
for b1 being Relation holds b1 |_2 {} = {} by Lemma40;

theorem Th195: :: ORDERS_1:195
for b1 being Function
for b2 being set st b2 is finite & b2 c= rng b1 holds
ex b3 being set st
( b3 c= dom b1 & b3 is finite & b1 .: b3 = b2 )
proof end;