:: ORDERS_2 semantic presentation

definition
attr a1 is strict;
struct RelStr -> 1-sorted ;
aggr RelStr(# carrier, InternalRel #) -> RelStr ;
sel InternalRel c1 -> Relation of the carrier of a1;
end;

registration
let c1 be non empty set ;
let c2 be Relation of c1;
cluster RelStr(# a1,a2 #) -> non empty ;
coherence
not RelStr(# c1,c2 #) is empty
proof end;
end;

definition
let c1 be RelStr ;
canceled;
canceled;
canceled;
attr a1 is reflexive means :Def4: :: ORDERS_2:def 4
the InternalRel of a1 is_reflexive_in the carrier of a1;
attr a1 is transitive means :Def5: :: ORDERS_2:def 5
the InternalRel of a1 is_transitive_in the carrier of a1;
attr a1 is antisymmetric means :Def6: :: ORDERS_2:def 6
the InternalRel of a1 is_antisymmetric_in the carrier of a1;
end;

:: deftheorem Def1 ORDERS_2:def 1 :
canceled;

:: deftheorem Def2 ORDERS_2:def 2 :
canceled;

:: deftheorem Def3 ORDERS_2:def 3 :
canceled;

:: deftheorem Def4 defines reflexive ORDERS_2:def 4 :
for b1 being RelStr holds
( b1 is reflexive iff the InternalRel of b1 is_reflexive_in the carrier of b1 );

:: deftheorem Def5 defines transitive ORDERS_2:def 5 :
for b1 being RelStr holds
( b1 is transitive iff the InternalRel of b1 is_transitive_in the carrier of b1 );

:: deftheorem Def6 defines antisymmetric ORDERS_2:def 6 :
for b1 being RelStr holds
( b1 is antisymmetric iff the InternalRel of b1 is_antisymmetric_in the carrier of b1 );

registration
cluster non empty strict reflexive transitive antisymmetric RelStr ;
existence
ex b1 being RelStr st
( not b1 is empty & b1 is reflexive & b1 is transitive & b1 is antisymmetric & b1 is strict )
proof end;
end;

definition
mode Poset is reflexive transitive antisymmetric RelStr ;
end;

registration
let c1 be Poset;
cluster the InternalRel of a1 -> reflexive antisymmetric transitive total ;
coherence
( the InternalRel of c1 is total & the InternalRel of c1 is reflexive & the InternalRel of c1 is antisymmetric & the InternalRel of c1 is transitive )
proof end;
end;

registration
let c1 be set ;
let c2 be Order of c1;
cluster RelStr(# a1,a2 #) -> reflexive transitive antisymmetric ;
coherence
( RelStr(# c1,c2 #) is reflexive & RelStr(# c1,c2 #) is transitive & RelStr(# c1,c2 #) is antisymmetric )
proof end;
end;

Lemma4: for b1 being set
for b2 being non empty Poset
for b3 being Subset of b2 st b1 in b3 holds
b1 is Element of b2
;

definition
let c1 be RelStr ;
let c2, c3 be Element of c1;
canceled;
canceled;
pred c2 <= c3 means :Def9: :: ORDERS_2:def 9
[a2,a3] in the InternalRel of a1;
end;

:: deftheorem Def7 ORDERS_2:def 7 :
canceled;

:: deftheorem Def8 ORDERS_2:def 8 :
canceled;

:: deftheorem Def9 defines <= ORDERS_2:def 9 :
for b1 being RelStr
for b2, b3 being Element of b1 holds
( b2 <= b3 iff [b2,b3] in the InternalRel of b1 );

notation
let c1 be RelStr ;
let c2, c3 be Element of c1;
synonym c3 >= c2 for c2 <= c3;
end;

definition
let c1 be RelStr ;
let c2, c3 be Element of c1;
pred c2 < c3 means :Def10: :: ORDERS_2:def 10
( a2 <= a3 & a2 <> a3 );
irreflexivity
for b1 being Element of c1 holds
( not b1 <= b1 or not b1 <> b1 ) ;
end;

:: deftheorem Def10 defines < ORDERS_2:def 10 :
for b1 being RelStr
for b2, b3 being Element of b1 holds
( b2 < b3 iff ( b2 <= b3 & b2 <> b3 ) );

notation
let c1 be RelStr ;
let c2, c3 be Element of c1;
synonym c3 > c2 for c2 < c3;
end;

theorem Th1: :: ORDERS_2:1
canceled;

theorem Th2: :: ORDERS_2:2
canceled;

theorem Th3: :: ORDERS_2:3
canceled;

theorem Th4: :: ORDERS_2:4
canceled;

theorem Th5: :: ORDERS_2:5
canceled;

theorem Th6: :: ORDERS_2:6
canceled;

theorem Th7: :: ORDERS_2:7
canceled;

theorem Th8: :: ORDERS_2:8
canceled;

theorem Th9: :: ORDERS_2:9
canceled;

theorem Th10: :: ORDERS_2:10
canceled;

theorem Th11: :: ORDERS_2:11
canceled;

theorem Th12: :: ORDERS_2:12
canceled;

theorem Th13: :: ORDERS_2:13
canceled;

theorem Th14: :: ORDERS_2:14
canceled;

theorem Th15: :: ORDERS_2:15
canceled;

theorem Th16: :: ORDERS_2:16
canceled;

theorem Th17: :: ORDERS_2:17
canceled;

theorem Th18: :: ORDERS_2:18
canceled;

theorem Th19: :: ORDERS_2:19
canceled;

theorem Th20: :: ORDERS_2:20
canceled;

theorem Th21: :: ORDERS_2:21
canceled;

theorem Th22: :: ORDERS_2:22
canceled;

theorem Th23: :: ORDERS_2:23
canceled;

theorem Th24: :: ORDERS_2:24
for b1 being non empty reflexive RelStr
for b2 being Element of b1 holds b2 <= b2
proof end;

definition
let c1 be non empty reflexive RelStr ;
let c2, c3 be Element of c1;
redefine pred <= as c2 <= c3;
reflexivity
for b1 being Element of c1 holds b1 <= b1 by Th24;
end;

theorem Th25: :: ORDERS_2:25
for b1 being antisymmetric RelStr
for b2, b3 being Element of b1 st b2 <= b3 & b3 <= b2 holds
b2 = b3
proof end;

theorem Th26: :: ORDERS_2:26
for b1 being transitive RelStr
for b2, b3, b4 being Element of b1 st b2 <= b3 & b3 <= b4 holds
b2 <= b4
proof end;

theorem Th27: :: ORDERS_2:27
canceled;

theorem Th28: :: ORDERS_2:28
for b1 being antisymmetric RelStr
for b2, b3 being Element of b1 holds
( not b2 < b3 or not b3 < b2 )
proof end;

theorem Th29: :: ORDERS_2:29
for b1 being transitive antisymmetric RelStr
for b2, b3, b4 being Element of b1 st b2 < b3 & b3 < b4 holds
b2 < b4
proof end;

theorem Th30: :: ORDERS_2:30
for b1 being antisymmetric RelStr
for b2, b3 being Element of b1 st b2 <= b3 holds
not b3 < b2
proof end;

theorem Th31: :: ORDERS_2:31
canceled;

theorem Th32: :: ORDERS_2:32
for b1 being transitive antisymmetric RelStr
for b2, b3, b4 being Element of b1 st ( ( b2 < b3 & b3 <= b4 ) or ( b2 <= b3 & b3 < b4 ) ) holds
b2 < b4
proof end;

definition
let c1 be RelStr ;
let c2 be Subset of c1;
attr a2 is strongly_connected means :Def11: :: ORDERS_2:def 11
the InternalRel of a1 is_strongly_connected_in a2;
end;

:: deftheorem Def11 defines strongly_connected ORDERS_2:def 11 :
for b1 being RelStr
for b2 being Subset of b1 holds
( b2 is strongly_connected iff the InternalRel of b1 is_strongly_connected_in b2 );

registration
let c1 be RelStr ;
cluster {} a1 -> strongly_connected ;
coherence
{} c1 is strongly_connected
proof end;
end;

registration
let c1 be RelStr ;
cluster strongly_connected Element of bool the carrier of a1;
existence
ex b1 being Subset of c1 st b1 is strongly_connected
proof end;
end;

definition
let c1 be RelStr ;
mode Chain of a1 is strongly_connected Subset of a1;
end;

theorem Th33: :: ORDERS_2:33
canceled;

theorem Th34: :: ORDERS_2:34
canceled;

theorem Th35: :: ORDERS_2:35
for b1 being non empty reflexive RelStr
for b2 being Element of b1 holds {b2} is Chain of b1
proof end;

theorem Th36: :: ORDERS_2:36
for b1 being non empty reflexive RelStr
for b2, b3 being Element of b1 holds
( {b2,b3} is Chain of b1 iff ( b2 <= b3 or b3 <= b2 ) )
proof end;

theorem Th37: :: ORDERS_2:37
for b1 being RelStr
for b2 being Chain of b1
for b3 being Subset of b1 st b3 c= b2 holds
b3 is Chain of b1
proof end;

theorem Th38: :: ORDERS_2:38
for b1 being reflexive RelStr
for b2, b3 being Element of b1 holds
( ( b2 <= b3 or b3 <= b2 ) iff ex b4 being Chain of b1 st
( b2 in b4 & b3 in b4 ) )
proof end;

theorem Th39: :: ORDERS_2:39
for b1 being reflexive antisymmetric RelStr
for b2, b3 being Element of b1 holds
( ex b4 being Chain of b1 st
( b2 in b4 & b3 in b4 ) iff ( b2 < b3 iff not b3 <= b2 ) )
proof end;

theorem Th40: :: ORDERS_2:40
for b1 being RelStr
for b2 being Subset of b1 st the InternalRel of b1 well_orders b2 holds
b2 is Chain of b1
proof end;

definition
let c1 be non empty Poset;
let c2 be Subset of c1;
func UpperCone c2 -> Subset of a1 equals :: ORDERS_2:def 12
{ b1 where B is Element of a1 : for b1 being Element of a1 st b2 in a2 holds
b2 < b1 } ;
coherence
{ b1 where B is Element of c1 : for b1 being Element of c1 st b2 in c2 holds
b2 < b1 } is Subset of c1
proof end;
end;

:: deftheorem Def12 defines UpperCone ORDERS_2:def 12 :
for b1 being non empty Poset
for b2 being Subset of b1 holds UpperCone b2 = { b3 where B is Element of b1 : for b1 being Element of b1 st b4 in b2 holds
b4 < b3 } ;

definition
let c1 be non empty Poset;
let c2 be Subset of c1;
func LowerCone c2 -> Subset of a1 equals :: ORDERS_2:def 13
{ b1 where B is Element of a1 : for b1 being Element of a1 st b2 in a2 holds
b1 < b2 } ;
coherence
{ b1 where B is Element of c1 : for b1 being Element of c1 st b2 in c2 holds
b1 < b2 } is Subset of c1
proof end;
end;

:: deftheorem Def13 defines LowerCone ORDERS_2:def 13 :
for b1 being non empty Poset
for b2 being Subset of b1 holds LowerCone b2 = { b3 where B is Element of b1 : for b1 being Element of b1 st b4 in b2 holds
b3 < b4 } ;

theorem Th41: :: ORDERS_2:41
canceled;

theorem Th42: :: ORDERS_2:42
canceled;

theorem Th43: :: ORDERS_2:43
for b1 being non empty Poset holds UpperCone ({} b1) = the carrier of b1
proof end;

theorem Th44: :: ORDERS_2:44
for b1 being non empty Poset holds UpperCone ([#] b1) = {}
proof end;

theorem Th45: :: ORDERS_2:45
for b1 being non empty Poset holds LowerCone ({} b1) = the carrier of b1
proof end;

theorem Th46: :: ORDERS_2:46
for b1 being non empty Poset holds LowerCone ([#] b1) = {}
proof end;

theorem Th47: :: ORDERS_2:47
for b1 being non empty Poset
for b2 being Element of b1
for b3 being Subset of b1 st b2 in b3 holds
not b2 in UpperCone b3
proof end;

theorem Th48: :: ORDERS_2:48
for b1 being non empty Poset
for b2 being Element of b1 holds not b2 in UpperCone {b2}
proof end;

theorem Th49: :: ORDERS_2:49
for b1 being non empty Poset
for b2 being Element of b1
for b3 being Subset of b1 st b2 in b3 holds
not b2 in LowerCone b3
proof end;

theorem Th50: :: ORDERS_2:50
for b1 being non empty Poset
for b2 being Element of b1 holds not b2 in LowerCone {b2}
proof end;

theorem Th51: :: ORDERS_2:51
for b1 being non empty Poset
for b2, b3 being Element of b1 holds
( b2 < b3 iff b3 in UpperCone {b2} )
proof end;

theorem Th52: :: ORDERS_2:52
for b1 being non empty Poset
for b2, b3 being Element of b1 holds
( b2 < b3 iff b2 in LowerCone {b3} )
proof end;

definition
let c1 be non empty Poset;
let c2 be Subset of c1;
let c3 be Element of c1;
func InitSegm c2,c3 -> Subset of a1 equals :: ORDERS_2:def 14
(LowerCone {a3}) /\ a2;
correctness
coherence
(LowerCone {c3}) /\ c2 is Subset of c1;
;
end;

:: deftheorem Def14 defines InitSegm ORDERS_2:def 14 :
for b1 being non empty Poset
for b2 being Subset of b1
for b3 being Element of b1 holds InitSegm b2,b3 = (LowerCone {b3}) /\ b2;

definition
let c1 be non empty Poset;
let c2 be Subset of c1;
mode Initial_Segm of c2 -> Subset of a1 means :Def15: :: ORDERS_2:def 15
ex b1 being Element of a1 st
( b1 in a2 & a3 = InitSegm a2,b1 ) if a2 <> {}
otherwise a3 = {} ;
existence
( ( c2 <> {} implies ex b1 being Subset of c1ex b2 being Element of c1 st
( b2 in c2 & b1 = InitSegm c2,b2 ) ) & ( not c2 <> {} implies ex b1 being Subset of c1 st b1 = {} ) )
proof end;
consistency
for b1 being Subset of c1 holds verum ;
end;

:: deftheorem Def15 defines Initial_Segm ORDERS_2:def 15 :
for b1 being non empty Poset
for b2, b3 being Subset of b1 holds
( ( b2 <> {} implies ( b3 is Initial_Segm of b2 iff ex b4 being Element of b1 st
( b4 in b2 & b3 = InitSegm b2,b4 ) ) ) & ( not b2 <> {} implies ( b3 is Initial_Segm of b2 iff b3 = {} ) ) );

theorem Th53: :: ORDERS_2:53
canceled;

theorem Th54: :: ORDERS_2:54
canceled;

theorem Th55: :: ORDERS_2:55
canceled;

theorem Th56: :: ORDERS_2:56
for b1 being set
for b2 being non empty Poset
for b3 being Element of b2
for b4 being Subset of b2 holds
( b1 in InitSegm b4,b3 iff ( b1 in LowerCone {b3} & b1 in b4 ) ) by XBOOLE_0:def 3;

theorem Th57: :: ORDERS_2:57
for b1 being non empty Poset
for b2, b3 being Element of b1
for b4 being Subset of b1 holds
( b2 in InitSegm b4,b3 iff ( b2 < b3 & b2 in b4 ) )
proof end;

theorem Th58: :: ORDERS_2:58
canceled;

theorem Th59: :: ORDERS_2:59
canceled;

theorem Th60: :: ORDERS_2:60
for b1 being non empty Poset
for b2 being Element of b1 holds InitSegm ({} b1),b2 = {} ;

theorem Th61: :: ORDERS_2:61
for b1 being non empty Poset
for b2 being Element of b1
for b3 being Subset of b1 holds InitSegm b3,b2 c= b3 by XBOOLE_1:17;

theorem Th62: :: ORDERS_2:62
for b1 being non empty Poset
for b2 being Element of b1
for b3 being Subset of b1 holds not b2 in InitSegm b3,b2
proof end;

theorem Th63: :: ORDERS_2:63
canceled;

theorem Th64: :: ORDERS_2:64
for b1 being non empty Poset
for b2, b3 being Element of b1
for b4 being Subset of b1 st b2 < b3 holds
InitSegm b4,b2 c= InitSegm b4,b3
proof end;

theorem Th65: :: ORDERS_2:65
for b1 being non empty Poset
for b2 being Element of b1
for b3, b4 being Subset of b1 st b3 c= b4 holds
InitSegm b3,b2 c= InitSegm b4,b2
proof end;

theorem Th66: :: ORDERS_2:66
canceled;

theorem Th67: :: ORDERS_2:67
for b1 being non empty Poset
for b2 being Subset of b1
for b3 being Initial_Segm of b2 holds b3 c= b2
proof end;

theorem Th68: :: ORDERS_2:68
for b1 being non empty Poset
for b2 being Subset of b1 holds
( b2 <> {} iff not b2 is Initial_Segm of b2 )
proof end;

theorem Th69: :: ORDERS_2:69
for b1 being non empty Poset
for b2, b3 being Subset of b1 st ( b2 <> {} or b3 <> {} ) & b2 is Initial_Segm of b3 holds
not b3 is Initial_Segm of b2
proof end;

theorem Th70: :: ORDERS_2:70
for b1 being non empty Poset
for b2, b3 being Element of b1
for b4, b5 being Subset of b1 st b2 < b3 & b2 in b4 & b3 in b5 & b5 is Initial_Segm of b4 holds
b2 in b5
proof end;

theorem Th71: :: ORDERS_2:71
for b1 being non empty Poset
for b2 being Element of b1
for b3, b4 being Subset of b1 st b2 in b3 & b3 is Initial_Segm of b4 holds
InitSegm b3,b2 = InitSegm b4,b2
proof end;

theorem Th72: :: ORDERS_2:72
for b1 being non empty Poset
for b2, b3 being Subset of b1 st b2 c= b3 & the InternalRel of b1 well_orders b3 & ( for b4, b5 being Element of b1 st b5 in b2 & b4 < b5 holds
b4 in b2 ) & not b2 = b3 holds
b2 is Initial_Segm of b3
proof end;

theorem Th73: :: ORDERS_2:73
for b1 being non empty Poset
for b2, b3 being Subset of b1 st b2 c= b3 & the InternalRel of b1 well_orders b3 & ( for b4, b5 being Element of b1 st b5 in b2 & b4 in b3 & b4 < b5 holds
b4 in b2 ) & not b2 = b3 holds
b2 is Initial_Segm of b3
proof end;

definition
let c1 be non empty Poset;
let c2 be Choice_Function of BOOL the carrier of c1;
mode Chain of c2 -> Chain of a1 means :Def16: :: ORDERS_2:def 16
( a3 <> {} & the InternalRel of a1 well_orders a3 & ( for b1 being Element of a1 st b1 in a3 holds
a2 . (UpperCone (InitSegm a3,b1)) = b1 ) );
existence
ex b1 being Chain of c1 st
( b1 <> {} & the InternalRel of c1 well_orders b1 & ( for b2 being Element of c1 st b2 in b1 holds
c2 . (UpperCone (InitSegm b1,b2)) = b2 ) )
proof end;
end;

:: deftheorem Def16 defines Chain ORDERS_2:def 16 :
for b1 being non empty Poset
for b2 being Choice_Function of BOOL the carrier of b1
for b3 being Chain of b1 holds
( b3 is Chain of b2 iff ( b3 <> {} & the InternalRel of b1 well_orders b3 & ( for b4 being Element of b1 st b4 in b3 holds
b2 . (UpperCone (InitSegm b3,b4)) = b4 ) ) );

theorem Th74: :: ORDERS_2:74
canceled;

theorem Th75: :: ORDERS_2:75
canceled;

theorem Th76: :: ORDERS_2:76
canceled;

theorem Th77: :: ORDERS_2:77
canceled;

theorem Th78: :: ORDERS_2:78
for b1 being non empty Poset
for b2 being Choice_Function of BOOL the carrier of b1 holds {(b2 . the carrier of b1)} is Chain of b2
proof end;

theorem Th79: :: ORDERS_2:79
for b1 being non empty Poset
for b2 being Choice_Function of BOOL the carrier of b1
for b3 being Chain of b2 holds b2 . the carrier of b1 in b3
proof end;

theorem Th80: :: ORDERS_2:80
for b1 being non empty Poset
for b2, b3 being Element of b1
for b4 being Choice_Function of BOOL the carrier of b1
for b5 being Chain of b4 st b2 in b5 & b3 = b4 . the carrier of b1 holds
b3 <= b2
proof end;

theorem Th81: :: ORDERS_2:81
for b1 being non empty Poset
for b2 being Element of b1
for b3 being Choice_Function of BOOL the carrier of b1
for b4 being Chain of b3 st b2 = b3 . the carrier of b1 holds
InitSegm b4,b2 = {}
proof end;

theorem Th82: :: ORDERS_2:82
for b1 being non empty Poset
for b2 being Choice_Function of BOOL the carrier of b1
for b3, b4 being Chain of b2 holds b3 meets b4
proof end;

theorem Th83: :: ORDERS_2:83
for b1 being non empty Poset
for b2 being Choice_Function of BOOL the carrier of b1
for b3, b4 being Chain of b2 st b3 <> b4 holds
( b3 is Initial_Segm of b4 iff b4 is not Initial_Segm of b3 )
proof end;

theorem Th84: :: ORDERS_2:84
for b1 being non empty Poset
for b2 being Choice_Function of BOOL the carrier of b1
for b3, b4 being Chain of b2 holds
( b3 c< b4 iff b3 is Initial_Segm of b4 )
proof end;

definition
let c1 be non empty Poset;
let c2 be Choice_Function of BOOL the carrier of c1;
func Chains c2 -> set means :Def17: :: ORDERS_2:def 17
for b1 being set holds
( b1 in a3 iff b1 is Chain of a2 );
existence
ex b1 being set st
for b2 being set holds
( b2 in b1 iff b2 is Chain of c2 )
proof end;
uniqueness
for b1, b2 being set st ( for b3 being set holds
( b3 in b1 iff b3 is Chain of c2 ) ) & ( for b3 being set holds
( b3 in b2 iff b3 is Chain of c2 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def17 defines Chains ORDERS_2:def 17 :
for b1 being non empty Poset
for b2 being Choice_Function of BOOL the carrier of b1
for b3 being set holds
( b3 = Chains b2 iff for b4 being set holds
( b4 in b3 iff b4 is Chain of b2 ) );

registration
let c1 be non empty Poset;
let c2 be Choice_Function of BOOL the carrier of c1;
cluster Chains a2 -> non empty ;
coherence
not Chains c2 is empty
proof end;
end;

Lemma44: for b1 being non empty Poset
for b2 being Choice_Function of BOOL the carrier of b1 holds union (Chains b2) is Subset of b1
proof end;

Lemma45: for b1 being non empty Poset
for b2 being Choice_Function of BOOL the carrier of b1 holds union (Chains b2) is Chain of b1
proof end;

theorem Th85: :: ORDERS_2:85
canceled;

theorem Th86: :: ORDERS_2:86
canceled;

theorem Th87: :: ORDERS_2:87
for b1 being non empty Poset
for b2 being Choice_Function of BOOL the carrier of b1 holds union (Chains b2) <> {}
proof end;

theorem Th88: :: ORDERS_2:88
for b1 being non empty Poset
for b2 being Subset of b1
for b3 being Choice_Function of BOOL the carrier of b1
for b4 being Chain of b3 st b4 <> union (Chains b3) & b2 = union (Chains b3) holds
b4 is Initial_Segm of b2
proof end;

theorem Th89: :: ORDERS_2:89
for b1 being non empty Poset
for b2 being Choice_Function of BOOL the carrier of b1 holds union (Chains b2) is Chain of b2
proof end;

theorem Th90: :: ORDERS_2:90
canceled;

theorem Th91: :: ORDERS_2:91
canceled;

theorem Th92: :: ORDERS_2:92
canceled;

theorem Th93: :: ORDERS_2:93
canceled;

theorem Th94: :: ORDERS_2:94
canceled;

theorem Th95: :: ORDERS_2:95
canceled;

theorem Th96: :: ORDERS_2:96
canceled;

theorem Th97: :: ORDERS_2:97
canceled;

theorem Th98: :: ORDERS_2:98
canceled;

theorem Th99: :: ORDERS_2:99
canceled;

theorem Th100: :: ORDERS_2:100
canceled;

theorem Th101: :: ORDERS_2:101
canceled;

theorem Th102: :: ORDERS_2:102
canceled;

theorem Th103: :: ORDERS_2:103
canceled;

theorem Th104: :: ORDERS_2:104
canceled;

theorem Th105: :: ORDERS_2:105
canceled;

theorem Th106: :: ORDERS_2:106
canceled;

theorem Th107: :: ORDERS_2:107
for b1 being non empty Poset
for b2 being Subset of b1 holds field (the InternalRel of b1 |_2 b2) = b2
proof end;

theorem Th108: :: ORDERS_2:108
for b1 being non empty Poset
for b2 being Subset of b1 st the InternalRel of b1 |_2 b2 is_linear-order holds
b2 is Chain of b1
proof end;

theorem Th109: :: ORDERS_2:109
for b1 being non empty Poset
for b2 being Chain of b1 holds the InternalRel of b1 |_2 b2 is_linear-order
proof end;

theorem Th110: :: ORDERS_2:110
canceled;

theorem Th111: :: ORDERS_2:111
canceled;

theorem Th112: :: ORDERS_2:112
canceled;

theorem Th113: :: ORDERS_2:113
canceled;

theorem Th114: :: ORDERS_2:114
canceled;

theorem Th115: :: ORDERS_2:115
canceled;

theorem Th116: :: ORDERS_2:116
canceled;

theorem Th117: :: ORDERS_2:117
canceled;

theorem Th118: :: ORDERS_2:118
canceled;

theorem Th119: :: ORDERS_2:119
canceled;

theorem Th120: :: ORDERS_2:120
canceled;

theorem Th121: :: ORDERS_2:121
canceled;

theorem Th122: :: ORDERS_2:122
canceled;

theorem Th123: :: ORDERS_2:123
canceled;

theorem Th124: :: ORDERS_2:124
canceled;

theorem Th125: :: ORDERS_2:125
canceled;

theorem Th126: :: ORDERS_2:126
canceled;

theorem Th127: :: ORDERS_2:127
canceled;

theorem Th128: :: ORDERS_2:128
canceled;

theorem Th129: :: ORDERS_2:129
canceled;

theorem Th130: :: ORDERS_2:130
canceled;

theorem Th131: :: ORDERS_2:131
canceled;

theorem Th132: :: ORDERS_2:132
canceled;

theorem Th133: :: ORDERS_2:133
canceled;

theorem Th134: :: ORDERS_2:134
canceled;

theorem Th135: :: ORDERS_2:135
for b1 being non empty Poset
for b2 being Subset of b1 st the InternalRel of b1 linearly_orders b2 holds
b2 is Chain of b1
proof end;

theorem Th136: :: ORDERS_2:136
for b1 being non empty Poset
for b2 being Chain of b1 holds the InternalRel of b1 linearly_orders b2
proof end;

theorem Th137: :: ORDERS_2:137
canceled;

theorem Th138: :: ORDERS_2:138
canceled;

theorem Th139: :: ORDERS_2:139
canceled;

theorem Th140: :: ORDERS_2:140
canceled;

theorem Th141: :: ORDERS_2:141
canceled;

theorem Th142: :: ORDERS_2:142
canceled;

theorem Th143: :: ORDERS_2:143
canceled;

theorem Th144: :: ORDERS_2:144
canceled;

theorem Th145: :: ORDERS_2:145
canceled;

theorem Th146: :: ORDERS_2:146
canceled;

theorem Th147: :: ORDERS_2:147
canceled;

theorem Th148: :: ORDERS_2:148
canceled;

theorem Th149: :: ORDERS_2:149
canceled;

theorem Th150: :: ORDERS_2:150
canceled;

theorem Th151: :: ORDERS_2:151
canceled;

theorem Th152: :: ORDERS_2:152
canceled;

theorem Th153: :: ORDERS_2:153
canceled;

theorem Th154: :: ORDERS_2:154
canceled;

theorem Th155: :: ORDERS_2:155
canceled;

theorem Th156: :: ORDERS_2:156
canceled;

theorem Th157: :: ORDERS_2:157
canceled;

theorem Th158: :: ORDERS_2:158
for b1 being non empty Poset
for b2 being Element of b1 holds
( b2 is_minimal_in the InternalRel of b1 iff for b3 being Element of b1 holds not b3 < b2 )
proof end;

theorem Th159: :: ORDERS_2:159
for b1 being non empty Poset
for b2 being Element of b1 holds
( b2 is_maximal_in the InternalRel of b1 iff for b3 being Element of b1 holds not b2 < b3 )
proof end;

theorem Th160: :: ORDERS_2:160
for b1 being non empty Poset
for b2 being Element of b1 holds
( b2 is_superior_of the InternalRel of b1 iff for b3 being Element of b1 st b2 <> b3 holds
b3 < b2 )
proof end;

theorem Th161: :: ORDERS_2:161
for b1 being non empty Poset
for b2 being Element of b1 holds
( b2 is_inferior_of the InternalRel of b1 iff for b3 being Element of b1 st b2 <> b3 holds
b2 < b3 )
proof end;

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

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

theorem Th162: :: ORDERS_2:162
for b1 being non empty Poset st ( for b2 being Chain of b1 ex b3 being Element of b1 st
for b4 being Element of b1 st b4 in b2 holds
b4 <= b3 ) holds
ex b2 being Element of b1 st
for b3 being Element of b1 holds not b2 < b3
proof end;

theorem Th163: :: ORDERS_2:163
for b1 being non empty Poset st ( for b2 being Chain of b1 ex b3 being Element of b1 st
for b4 being Element of b1 st b4 in b2 holds
b3 <= b4 ) holds
ex b2 being Element of b1 st
for b3 being Element of b1 holds not b3 < b2
proof end;