:: ORDERS_2 semantic presentation

begin


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

registration
let X be non empty set ;
let R be Relation of X;
cluster RelStr(# X,R #) ->  non empty ;
coherence
 not RelStr(# X,R #) is empty ;
end;

definition
let A be RelStr ;
attrA is total  means :Def1: :: ORDERS_2:def 1
 the InternalRel of A is total ;
attrA is reflexive  means :Def2: :: ORDERS_2:def 2
 the InternalRel of A is_reflexive_in the carrier of A;
attrA is transitive  means :Def3: :: ORDERS_2:def 3
 the InternalRel of A is_transitive_in the carrier of A;
attrA is antisymmetric  means :Def4: :: ORDERS_2:def 4
 the InternalRel of A is_antisymmetric_in the carrier of A;
end;

:: deftheorem Def1 defines total ORDERS_2:def_1_:_
 for A being RelStr holds
( A is total iff the InternalRel of A is total );

:: deftheorem Def2 defines reflexive ORDERS_2:def_2_:_
 for A being RelStr holds
( A is reflexive iff the InternalRel of A is_reflexive_in the carrier of A );

:: deftheorem Def3 defines transitive ORDERS_2:def_3_:_
 for A being RelStr holds
( A is transitive iff the InternalRel of A is_transitive_in the carrier of A );

:: deftheorem Def4 defines antisymmetric ORDERS_2:def_4_:_
 for A being RelStr holds
( A is antisymmetric iff the InternalRel of A is_antisymmetric_in the carrier of A );

registration
cluster1 -element strict total reflexive transitive antisymmetric for RelStr ;
existence
 ex b1 being RelStr st
( b1 is reflexive & b1 is transitive & b1 is antisymmetric & b1 is strict & b1 is total & b1 is 1 -element )
proof
set R = the Order of {{}};
take L = RelStr(# {{}}, the Order of {{}} #); ::_thesis: ( L is reflexive & L is transitive & L is antisymmetric & L is strict & L is total & L is 1 -element )
A1: field the Order of {{}} = the carrier of L by ORDERS_1:12;
hence  the InternalRel of L is_reflexive_in the carrier of L by RELAT_2:def_9; :: according to ORDERS_2:def_2 ::_thesis: ( L is transitive & L is antisymmetric & L is strict & L is total & L is 1 -element )
thus  the InternalRel of L is_transitive_in the carrier of L by A1, RELAT_2:def_16; :: according to ORDERS_2:def_3 ::_thesis: ( L is antisymmetric & L is strict & L is total & L is 1 -element )
thus  the InternalRel of L is_antisymmetric_in the carrier of L by A1, RELAT_2:def_12; :: according to ORDERS_2:def_4 ::_thesis: ( L is strict & L is total & L is 1 -element )
thus  L is strict ; ::_thesis: ( L is total & L is 1 -element )
thus  the InternalRel of L is total ; :: according to ORDERS_2:def_1 ::_thesis: L is 1 -element
thus  the carrier of L is 1 -element ; :: according to STRUCT_0:def_19 ::_thesis: verum
end;
end;

registration
cluster reflexive  ->  total for RelStr ;
coherence
 for b1 being RelStr st b1 is reflexive holds
b1 is total
proof
let L be RelStr ; ::_thesis: ( L is reflexive implies L is total )
assume  L is reflexive ; ::_thesis: L is total
then  the InternalRel of L is_reflexive_in the carrier of L by Def2;
then  dom the InternalRel of L = the carrier of L by ORDERS_1:13;
hence  the InternalRel of L is total by PARTFUN1:def_2; :: according to ORDERS_2:def_1 ::_thesis: verum
end;
end;

definition
mode Poset is reflexive transitive antisymmetric RelStr ;
end;

registration
let A be total RelStr ;
cluster the InternalRel of A ->  total ;
coherence
 the InternalRel of A is total by Def1;
end;

registration
let A be reflexive RelStr ;
cluster the InternalRel of A ->  reflexive ;
coherence
 the InternalRel of A is reflexive
proof
set R = the InternalRel of A;
 the InternalRel of A is_reflexive_in the carrier of A by Def2;
then A1: field the InternalRel of A = the carrier of A by ORDERS_1:13;
 the InternalRel of A is_reflexive_in the carrier of A by Def2;
hence  the InternalRel of A is reflexive by A1, RELAT_2:def_9; ::_thesis: verum
end;
end;

registration
let A be total antisymmetric RelStr ;
cluster the InternalRel of A ->  antisymmetric ;
coherence
 the InternalRel of A is antisymmetric
proof
set R = the InternalRel of A;
 ( field the InternalRel of A = the carrier of A & the InternalRel of A is_antisymmetric_in the carrier of A ) by Def4, ORDERS_1:12;
hence  the InternalRel of A is antisymmetric by RELAT_2:def_12; ::_thesis: verum
end;
end;

registration
let A be total transitive RelStr ;
cluster the InternalRel of A ->  transitive ;
coherence
 the InternalRel of A is transitive
proof
set R = the InternalRel of A;
 ( field the InternalRel of A = the carrier of A & the InternalRel of A is_transitive_in the carrier of A ) by Def3, ORDERS_1:12;
hence  the InternalRel of A is transitive by RELAT_2:def_16; ::_thesis: verum
end;
end;

registration
let X be set ;
let O be reflexive total Relation of X;
cluster RelStr(# X,O #) ->  reflexive ;
coherence
 RelStr(# X,O #) is reflexive
proof
set A = RelStr(# X,O #);
 field O = X by ORDERS_1:12;
hence  the InternalRel of RelStr(# X,O #) is_reflexive_in the carrier of RelStr(# X,O #) by RELAT_2:def_9; :: according to ORDERS_2:def_2 ::_thesis: verum
end;
end;

registration
let X be set ;
let O be transitive total Relation of X;
cluster RelStr(# X,O #) ->  transitive ;
coherence
 RelStr(# X,O #) is transitive
proof
set A = RelStr(# X,O #);
 field O = X by ORDERS_1:12;
hence  the InternalRel of RelStr(# X,O #) is_transitive_in the carrier of RelStr(# X,O #) by RELAT_2:def_16; :: according to ORDERS_2:def_3 ::_thesis: verum
end;
end;

registration
let X be set ;
let O be antisymmetric total Relation of X;
cluster RelStr(# X,O #) ->  antisymmetric ;
coherence
 RelStr(# X,O #) is antisymmetric
proof
set A = RelStr(# X,O #);
 field O = X by ORDERS_1:12;
hence  the InternalRel of RelStr(# X,O #) is_antisymmetric_in the carrier of RelStr(# X,O #) by RELAT_2:def_12; :: according to ORDERS_2:def_4 ::_thesis: verum
end;
end;

         Lm1:  for x being set
for A being non empty Poset
for S being Subset of A st x in S holds
x is Element of A
;

definition
let A be RelStr ;
let a1, a2 be Element of A;
preda1 <= a2 means :Def5: :: ORDERS_2:def 5
[a1,a2] in the InternalRel of A;
end;

:: deftheorem Def5 defines <= ORDERS_2:def_5_:_
 for A being RelStr
for a1, a2 being Element of A holds
( a1 <= a2 iff [a1,a2] in the InternalRel of A );

notation
let A be RelStr ;
let a1, a2 be Element of A;
synonym a2 >= a1 for a1 <= a2;
end;

definition
let A be RelStr ;
let a1, a2 be Element of A;
preda1 < a2 means :Def6: :: ORDERS_2:def 6
( a1 <= a2 & a1 <> a2 );
irreflexivity
 for a1 being Element of A holds
( not a1 <= a1 or not a1 <> a1 ) ;
end;

:: deftheorem Def6 defines < ORDERS_2:def_6_:_
 for A being RelStr
for a1, a2 being Element of A holds
( a1 < a2 iff ( a1 <= a2 & a1 <> a2 ) );

notation
let A be RelStr ;
let a1, a2 be Element of A;
synonym a2 > a1 for a1 < a2;
end;

theorem Th1: :: ORDERS_2:1
for A being non empty reflexive RelStr
for a being Element of A holds a <= a
proof
let A be non empty reflexive RelStr ; ::_thesis: for a being Element of A holds a <= a
let a be Element of A; ::_thesis: a <= a
 the InternalRel of A is_reflexive_in the carrier of A by Def2;
then  [a,a] in the InternalRel of A by RELAT_2:def_1;
hence  a <= a by Def5; ::_thesis: verum
end;

definition
let A be non empty reflexive RelStr ;
let a1, a2 be Element of A;
:: original: <=
redefine preda1 <= a2;
reflexivity
 for a1 being Element of A holds (A,b1,b1) by Th1;
end;

theorem Th2: :: ORDERS_2:2
for A being antisymmetric RelStr
for a1, a2 being Element of A st a1 <= a2 & a2 <= a1 holds
a1 = a2
proof
let A be antisymmetric RelStr ; ::_thesis: for a1, a2 being Element of A st a1 <= a2 & a2 <= a1 holds
a1 = a2
let a1, a2 be Element of A; ::_thesis: ( a1 <= a2 & a2 <= a1 implies a1 = a2 )
assume that
A1: [a1,a2] in the InternalRel of A and
A2: [a2,a1] in the InternalRel of A ; :: according to ORDERS_2:def_5 ::_thesis: a1 = a2
A3: the InternalRel of A is_antisymmetric_in the carrier of A by Def4;
 a1 in the carrier of A by A1, ZFMISC_1:87;
hence  a1 = a2 by A1, A2, A3, RELAT_2:def_4; ::_thesis: verum
end;

theorem Th3: :: ORDERS_2:3
for A being transitive RelStr
for a1, a2, a3 being Element of A st a1 <= a2 & a2 <= a3 holds
a1 <= a3
proof
let A be transitive RelStr ; ::_thesis: for a1, a2, a3 being Element of A st a1 <= a2 & a2 <= a3 holds
a1 <= a3
let a1, a2, a3 be Element of A; ::_thesis: ( a1 <= a2 & a2 <= a3 implies a1 <= a3 )
assume that
A1: [a1,a2] in the InternalRel of A and
A2: [a2,a3] in the InternalRel of A ; :: according to ORDERS_2:def_5 ::_thesis: a1 <= a3
A3: the InternalRel of A is_transitive_in the carrier of A by Def3;
 a1 in the carrier of A by A1, ZFMISC_1:87;
hence  [a1,a3] in the InternalRel of A by A1, A2, A3, RELAT_2:def_8; :: according to ORDERS_2:def_5 ::_thesis: verum
end;

theorem Th4: :: ORDERS_2:4
for A being antisymmetric RelStr
for a1, a2 being Element of A holds
( not a1 < a2 or not a2 < a1 )
proof
let A be antisymmetric RelStr ; ::_thesis: for a1, a2 being Element of A holds
( not a1 < a2 or not a2 < a1 )
let a1, a2 be Element of A; ::_thesis: ( not a1 < a2 or not a2 < a1 )
assume that
A1: a1 < a2 and
A2: a2 < a1 ; ::_thesis: contradiction
 ( a1 <= a2 & a2 <= a1 ) by A1, A2, Def6;
hence  contradiction by A1, Th2; ::_thesis: verum
end;

theorem Th5: :: ORDERS_2:5
for A being transitive antisymmetric RelStr
for a1, a2, a3 being Element of A st a1 < a2 & a2 < a3 holds
a1 < a3
proof
let A be transitive antisymmetric RelStr ; ::_thesis: for a1, a2, a3 being Element of A st a1 < a2 & a2 < a3 holds
a1 < a3
let a1, a2, a3 be Element of A; ::_thesis: ( a1 < a2 & a2 < a3 implies a1 < a3 )
assume A1: ( a1 < a2 & a2 < a3 ) ; ::_thesis: a1 < a3
then  ( a1 <= a2 & a2 <= a3 ) by Def6;
hence  a1 <= a3 by Th3; :: according to ORDERS_2:def_6 ::_thesis: a1 <> a3
thus  a1 <> a3 by A1, Th4; ::_thesis: verum
end;

theorem Th6: :: ORDERS_2:6
for A being antisymmetric RelStr
for a1, a2 being Element of A st a1 <= a2 holds
not a2 < a1
proof
let A be antisymmetric RelStr ; ::_thesis: for a1, a2 being Element of A st a1 <= a2 holds
not a2 < a1
let a1, a2 be Element of A; ::_thesis: ( a1 <= a2 implies not a2 < a1 )
assume that
A1: a1 <= a2 and
A2: a2 < a1 ; ::_thesis: contradiction
 a2 <= a1 by A2, Def6;
hence  contradiction by A1, A2, Th2; ::_thesis: verum
end;

theorem Th7: :: ORDERS_2:7
for A being transitive antisymmetric RelStr
for a1, a2, a3 being Element of A st ( ( a1 < a2 & a2 <= a3 ) or ( a1 <= a2 & a2 < a3 ) ) holds
a1 < a3
proof
let A be transitive antisymmetric RelStr ; ::_thesis: for a1, a2, a3 being Element of A st ( ( a1 < a2 & a2 <= a3 ) or ( a1 <= a2 & a2 < a3 ) ) holds
a1 < a3
let a1, a2, a3 be Element of A; ::_thesis: ( ( ( a1 < a2 & a2 <= a3 ) or ( a1 <= a2 & a2 < a3 ) ) implies a1 < a3 )
A1: now__::_thesis:_(_a1_<_a2_&_a2_<=_a3_&_(_(_a1_<_a2_&_a2_<=_a3_)_or_(_a1_<=_a2_&_a2_<_a3_)_)_implies_a1_<_a3_)
assume that
A2: a1 < a2 and
A3: a2 <= a3 ; ::_thesis: ( ( ( a1 < a2 & a2 <= a3 ) or ( a1 <= a2 & a2 < a3 ) ) implies a1 < a3 )
 a1 <= a2 by A2, Def6;
then  ( a1 <= a3 & a1 <> a3 ) by A2, A3, Th2, Th3;
hence  ( ( ( a1 < a2 & a2 <= a3 ) or ( a1 <= a2 & a2 < a3 ) ) implies a1 < a3 ) by Def6; ::_thesis: verum
end;
A4: now__::_thesis:_(_a1_<=_a2_&_a2_<_a3_&_(_(_a1_<_a2_&_a2_<=_a3_)_or_(_a1_<=_a2_&_a2_<_a3_)_)_implies_a1_<_a3_)
assume that
A5: a1 <= a2 and
A6: a2 < a3 ; ::_thesis: ( ( ( a1 < a2 & a2 <= a3 ) or ( a1 <= a2 & a2 < a3 ) ) implies a1 < a3 )
 a2 <= a3 by A6, Def6;
then  ( a1 <= a3 & a1 <> a3 ) by A5, A6, Th2, Th3;
hence  ( ( ( a1 < a2 & a2 <= a3 ) or ( a1 <= a2 & a2 < a3 ) ) implies a1 < a3 ) by Def6; ::_thesis: verum
end;
assume  ( ( a1 < a2 & a2 <= a3 ) or ( a1 <= a2 & a2 < a3 ) ) ; ::_thesis: a1 < a3
hence  a1 < a3 by A1, A4; ::_thesis: verum
end;

definition
let A be RelStr ;
let IT be Subset of A;
attrIT is strongly_connected  means :Def7: :: ORDERS_2:def 7
 the InternalRel of A is_strongly_connected_in IT;
end;

:: deftheorem Def7 defines strongly_connected ORDERS_2:def_7_:_
 for A being RelStr
for IT being Subset of A holds
( IT is strongly_connected iff the InternalRel of A is_strongly_connected_in IT );

registration
let A be RelStr ;
cluster empty  ->  strongly_connected for Element of bool the carrier of A;
coherence
 for b1 being Subset of A st b1 is empty holds
b1 is strongly_connected
proof
let S be Subset of A; ::_thesis: ( S is empty implies S is strongly_connected )
assume  S is empty ; ::_thesis: S is strongly_connected
then A1: S = {} A ;
let x1, x2 be set ; :: according to RELAT_2:def_7,ORDERS_2:def_7 ::_thesis: ( not x1 in S or not x2 in S or [x1,x2] in the InternalRel of A or [x2,x1] in the InternalRel of A )
thus  ( not x1 in S or not x2 in S or [x1,x2] in the InternalRel of A or [x2,x1] in the InternalRel of A ) by A1; ::_thesis: verum
end;
end;

registration
let A be RelStr ;
cluster strongly_connected for Element of bool the carrier of A;
existence
 ex b1 being Subset of A st b1 is strongly_connected
proof
take  {} A ; ::_thesis: {} A is strongly_connected
thus  {} A is strongly_connected ; ::_thesis: verum
end;
end;

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

theorem Th8: :: ORDERS_2:8
for A being non empty reflexive RelStr
for a being Element of A holds {a} is Chain of A
proof
let A be non empty reflexive RelStr ; ::_thesis: for a being Element of A holds {a} is Chain of A
let a be Element of A; ::_thesis: {a} is Chain of A
A1: the InternalRel of A is_reflexive_in the carrier of A by Def2;
 {a} is strongly_connected
proof
let x1, x2 be set ; :: according to RELAT_2:def_7,ORDERS_2:def_7 ::_thesis: ( not x1 in {a} or not x2 in {a} or [x1,x2] in the InternalRel of A or [x2,x1] in the InternalRel of A )
assume  ( x1 in {a} & x2 in {a} ) ; ::_thesis: ( [x1,x2] in the InternalRel of A or [x2,x1] in the InternalRel of A )
then  ( x1 = a & x2 = a ) by TARSKI:def_1;
hence  ( [x1,x2] in the InternalRel of A or [x2,x1] in the InternalRel of A ) by A1, RELAT_2:def_1; ::_thesis: verum
end;
hence  {a} is Chain of A ; ::_thesis: verum
end;

theorem Th9: :: ORDERS_2:9
for A being non empty reflexive RelStr
for a1, a2 being Element of A holds
( {a1,a2} is Chain of A iff ( a1 <= a2 or a2 <= a1 ) )
proof
let A be non empty reflexive RelStr ; ::_thesis: for a1, a2 being Element of A holds
( {a1,a2} is Chain of A iff ( a1 <= a2 or a2 <= a1 ) )
let a1, a2 be Element of A; ::_thesis: ( {a1,a2} is Chain of A iff ( a1 <= a2 or a2 <= a1 ) )
A1: a2 <= a2 ;
thus  ( not {a1,a2} is Chain of A or a1 <= a2 or a2 <= a1 ) ::_thesis: ( ( a1 <= a2 or a2 <= a1 ) implies {a1,a2} is Chain of A )
proof
assume  {a1,a2} is Chain of A ; ::_thesis: ( a1 <= a2 or a2 <= a1 )
then A2: the InternalRel of A is_strongly_connected_in {a1,a2} by Def7;
 ( a1 in {a1,a2} & a2 in {a1,a2} ) by TARSKI:def_2;
then  ( [a1,a2] in the InternalRel of A or [a2,a1] in the InternalRel of A ) by A2, RELAT_2:def_7;
hence  ( a1 <= a2 or a2 <= a1 ) by Def5; ::_thesis: verum
end;
assume A3: ( a1 <= a2 or a2 <= a1 ) ; ::_thesis: {a1,a2} is Chain of A
A4: a1 <= a1 ;
 {a1,a2} is strongly_connected
proof
let x be set ; :: according to RELAT_2:def_7,ORDERS_2:def_7 ::_thesis: for b1 being set holds
( not x in {a1,a2} or not b1 in {a1,a2} or [x,b1] in the InternalRel of A or [b1,x] in the InternalRel of A )
let y be set ; ::_thesis: ( not x in {a1,a2} or not y in {a1,a2} or [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
assume A5: ( x in {a1,a2} & y in {a1,a2} ) ; ::_thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
now__::_thesis:_(_[x,y]_in_the_InternalRel_of_A_or_[y,x]_in_the_InternalRel_of_A_)
percases ( ( x = a1 & y = a1 ) or ( x = a1 & y = a2 ) or ( x = a2 & y = a1 ) or ( x = a2 & y = a2 ) ) by A5, TARSKI:def_2;
suppose ( x = a1 & y = a1 ) ; ::_thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
hence  ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by A4, Def5; ::_thesis: verum
end;
suppose ( x = a1 & y = a2 ) ; ::_thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
hence  ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by A3, Def5; ::_thesis: verum
end;
suppose ( x = a2 & y = a1 ) ; ::_thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
hence  ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by A3, Def5; ::_thesis: verum
end;
suppose ( x = a2 & y = a2 ) ; ::_thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
hence  ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by A1, Def5; ::_thesis: verum
end;
end;
end;
hence  ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) ; ::_thesis: verum
end;
hence  {a1,a2} is Chain of A ; ::_thesis: verum
end;

theorem :: ORDERS_2:10
for A being RelStr
for C being Chain of A
for S being Subset of A st S c= C holds
S is Chain of A
proof
let A be RelStr ; ::_thesis: for C being Chain of A
for S being Subset of A st S c= C holds
S is Chain of A
let C be Chain of A; ::_thesis: for S being Subset of A st S c= C holds
S is Chain of A
let S be Subset of A; ::_thesis: ( S c= C implies S is Chain of A )
assume A1: S c= C ; ::_thesis: S is Chain of A
 the InternalRel of A is_strongly_connected_in C by Def7;
then  the InternalRel of A is_strongly_connected_in S by A1, ORDERS_1:11;
hence  S is Chain of A by Def7; ::_thesis: verum
end;

theorem Th11: :: ORDERS_2:11
for A being reflexive RelStr
for a1, a2 being Element of A holds
( ( a1 <= a2 or a2 <= a1 ) iff ex C being Chain of A st
( a1 in C & a2 in C ) )
proof
let A be reflexive RelStr ; ::_thesis: for a1, a2 being Element of A holds
( ( a1 <= a2 or a2 <= a1 ) iff ex C being Chain of A st
( a1 in C & a2 in C ) )
let a1, a2 be Element of A; ::_thesis: ( ( a1 <= a2 or a2 <= a1 ) iff ex C being Chain of A st
( a1 in C & a2 in C ) )
thus  ( for C being Chain of A holds
( not a1 in C or not a2 in C ) or a1 <= a2 or a2 <= a1 ) ::_thesis: ( ( a1 <= a2 or a2 <= a1 ) implies ex C being Chain of A st
( a1 in C & a2 in C ) )
proof
given C being Chain of A such that A1: ( a1 in C & a2 in C ) ; ::_thesis: ( a1 <= a2 or a2 <= a1 )
 the InternalRel of A is_strongly_connected_in C by Def7;
then  ( [a1,a2] in the InternalRel of A or [a2,a1] in the InternalRel of A ) by A1, RELAT_2:def_7;
hence  ( a1 <= a2 or a2 <= a1 ) by Def5; ::_thesis: verum
end;
assume A2: ( a1 <= a2 or a2 <= a1 ) ; ::_thesis: ex C being Chain of A st
( a1 in C & a2 in C )
then  ( [a1,a2] in the InternalRel of A or [a2,a1] in the InternalRel of A ) by Def5;
then reconsider B = A as non empty reflexive RelStr ;
reconsider b1 = a1, b2 = a2 as Element of B ;
reconsider Y = {b1,b2} as Chain of A by A2, Th9;
take  Y ; ::_thesis: ( a1 in Y & a2 in Y )
thus  ( a1 in Y & a2 in Y ) by TARSKI:def_2; ::_thesis: verum
end;

theorem Th12: :: ORDERS_2:12
for A being reflexive antisymmetric RelStr
for a1, a2 being Element of A holds
( ex C being Chain of A st
( a1 in C & a2 in C ) iff ( a1 < a2 iff not a2 <= a1 ) )
proof
let A be reflexive antisymmetric RelStr ; ::_thesis: for a1, a2 being Element of A holds
( ex C being Chain of A st
( a1 in C & a2 in C ) iff ( a1 < a2 iff not a2 <= a1 ) )
let a1, a2 be Element of A; ::_thesis: ( ex C being Chain of A st
( a1 in C & a2 in C ) iff ( a1 < a2 iff not a2 <= a1 ) )
thus  ( ex C being Chain of A st
( a1 in C & a2 in C ) implies ( a1 < a2 iff not a2 <= a1 ) ) ::_thesis: not ( ( a1 < a2 implies not a2 <= a1 ) & ( not a2 <= a1 implies a1 < a2 ) & ( for C being Chain of A holds
( not a1 in C or not a2 in C ) ) )
proof
given C being Chain of A such that A1: ( a1 in C & a2 in C ) ; ::_thesis: ( a1 < a2 iff not a2 <= a1 )
thus  ( a1 < a2 implies not a2 <= a1 ) by Th6; ::_thesis: ( not a2 <= a1 implies a1 < a2 )
assume that
A2: not a2 <= a1 and
A3: not a1 < a2 ; ::_thesis: contradiction
 ( not a1 <= a2 or a1 = a2 ) by A3, Def6;
hence  contradiction by A1, A2, Th11; ::_thesis: verum
end;
assume  ( a1 < a2 iff not a2 <= a1 ) ; ::_thesis: ex C being Chain of A st
( a1 in C & a2 in C )
then  ( a1 <= a2 or a2 <= a1 ) by Def6;
hence  ex C being Chain of A st
( a1 in C & a2 in C ) by Th11; ::_thesis: verum
end;

theorem Th13: :: ORDERS_2:13
for A being RelStr
for T being Subset of A st the InternalRel of A well_orders T holds
T is Chain of A
proof
let A be RelStr ; ::_thesis: for T being Subset of A st the InternalRel of A well_orders T holds
T is Chain of A
let T be Subset of A; ::_thesis: ( the InternalRel of A well_orders T implies T is Chain of A )
assume  the InternalRel of A well_orders T ; ::_thesis: T is Chain of A
then  ( the InternalRel of A is_connected_in T & the InternalRel of A is_reflexive_in T ) by WELLORD1:def_5;
then  the InternalRel of A is_strongly_connected_in T by ORDERS_1:7;
hence  T is Chain of A by Def7; ::_thesis: verum
end;

definition
let A be non empty Poset;
let S be Subset of A;
func UpperCone S ->  Subset of A equals :: ORDERS_2:def 8
 {  a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds
a2 < a1  }  ;
coherence
  {  a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds
a2 < a1  }  is Subset of A
proof
set T =  {  a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds
a2 < a1  }  ;
  {  a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds
a2 < a1  }  c= the carrier of A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds
a2 < a1  }  or x in the carrier of A )
assume  x in  {  a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds
a2 < a1  }  ; ::_thesis: x in the carrier of A
then  ex a1 being Element of A st
( x = a1 & ( for a2 being Element of A st a2 in S holds
a2 < a1 ) ) ;
hence  x in the carrier of A ; ::_thesis: verum
end;
hence   {  a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds
a2 < a1  }  is Subset of A ; ::_thesis: verum
end;
end;

:: deftheorem  defines UpperCone ORDERS_2:def_8_:_
 for A being non empty Poset
for S being Subset of A holds UpperCone S =  {  a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds
a2 < a1  }  ;

definition
let A be non empty Poset;
let S be Subset of A;
func LowerCone S ->  Subset of A equals :: ORDERS_2:def 9
 {  a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds
a1 < a2  }  ;
coherence
  {  a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds
a1 < a2  }  is Subset of A
proof
set T =  {  a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds
a1 < a2  }  ;
  {  a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds
a1 < a2  }  c= the carrier of A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds
a1 < a2  }  or x in the carrier of A )
assume  x in  {  a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds
a1 < a2  }  ; ::_thesis: x in the carrier of A
then  ex a1 being Element of A st
( x = a1 & ( for a2 being Element of A st a2 in S holds
a1 < a2 ) ) ;
hence  x in the carrier of A ; ::_thesis: verum
end;
hence   {  a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds
a1 < a2  }  is Subset of A ; ::_thesis: verum
end;
end;

:: deftheorem  defines LowerCone ORDERS_2:def_9_:_
 for A being non empty Poset
for S being Subset of A holds LowerCone S =  {  a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds
a1 < a2  }  ;

theorem Th14: :: ORDERS_2:14
for A being non empty Poset holds UpperCone ({} A) = the carrier of A
proof
let A be non empty Poset; ::_thesis: UpperCone ({} A) = the carrier of A
thus  UpperCone ({} A) c= the carrier of A ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of A c= UpperCone ({} A)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of A or x in UpperCone ({} A) )
assume  x in the carrier of A ; ::_thesis: x in UpperCone ({} A)
then reconsider a = x as Element of A ;
 for a2 being Element of A st a2 in {} A holds
a2 < a ;
hence  x in UpperCone ({} A) ; ::_thesis: verum
end;

theorem :: ORDERS_2:15
for A being non empty Poset holds UpperCone ([#] A) = {}
proof
let A be non empty Poset; ::_thesis: UpperCone ([#] A) = {}
thus  UpperCone ([#] A) c= {} :: according to XBOOLE_0:def_10 ::_thesis: {} c= UpperCone ([#] A)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in UpperCone ([#] A) or x in {} )
assume  x in UpperCone ([#] A) ; ::_thesis: x in {}
then  ex a being Element of A st
( x = a & ( for a2 being Element of A st a2 in [#] A holds
a2 < a ) ) ;
hence  x in {} ; ::_thesis: verum
end;
thus  {} c= UpperCone ([#] A) by XBOOLE_1:2; ::_thesis: verum
end;

theorem :: ORDERS_2:16
for A being non empty Poset holds LowerCone ({} A) = the carrier of A
proof
let A be non empty Poset; ::_thesis: LowerCone ({} A) = the carrier of A
thus  LowerCone ({} A) c= the carrier of A ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of A c= LowerCone ({} A)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of A or x in LowerCone ({} A) )
assume  x in the carrier of A ; ::_thesis: x in LowerCone ({} A)
then reconsider a = x as Element of A ;
 for a2 being Element of A st a2 in {} A holds
a < a2 ;
hence  x in LowerCone ({} A) ; ::_thesis: verum
end;

theorem :: ORDERS_2:17
for A being non empty Poset holds LowerCone ([#] A) = {}
proof
let A be non empty Poset; ::_thesis: LowerCone ([#] A) = {}
thus  LowerCone ([#] A) c= {} :: according to XBOOLE_0:def_10 ::_thesis: {} c= LowerCone ([#] A)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in LowerCone ([#] A) or x in {} )
assume  x in LowerCone ([#] A) ; ::_thesis: x in {}
then  ex a being Element of A st
( x = a & ( for a2 being Element of A st a2 in [#] A holds
a < a2 ) ) ;
hence  x in {} ; ::_thesis: verum
end;
thus  {} c= LowerCone ([#] A) by XBOOLE_1:2; ::_thesis: verum
end;

theorem Th18: :: ORDERS_2:18
for A being non empty Poset
for a being Element of A
for S being Subset of A st a in S holds
not a in UpperCone S
proof
let A be non empty Poset; ::_thesis: for a being Element of A
for S being Subset of A st a in S holds
not a in UpperCone S
let a be Element of A; ::_thesis: for S being Subset of A st a in S holds
not a in UpperCone S
let S be Subset of A; ::_thesis: ( a in S implies not a in UpperCone S )
assume that
A1: a in S and
A2: a in UpperCone S ; ::_thesis: contradiction
 ex a1 being Element of A st
( a1 = a & ( for a2 being Element of A st a2 in S holds
a2 < a1 ) ) by A2;
hence  contradiction by A1; ::_thesis: verum
end;

theorem :: ORDERS_2:19
for A being non empty Poset
for a being Element of A holds not a in UpperCone {a}
proof
let A be non empty Poset; ::_thesis: for a being Element of A holds not a in UpperCone {a}
let a be Element of A; ::_thesis: not a in UpperCone {a}
 a in {a} by TARSKI:def_1;
hence  not a in UpperCone {a} by Th18; ::_thesis: verum
end;

theorem Th20: :: ORDERS_2:20
for A being non empty Poset
for a being Element of A
for S being Subset of A st a in S holds
not a in LowerCone S
proof
let A be non empty Poset; ::_thesis: for a being Element of A
for S being Subset of A st a in S holds
not a in LowerCone S
let a be Element of A; ::_thesis: for S being Subset of A st a in S holds
not a in LowerCone S
let S be Subset of A; ::_thesis: ( a in S implies not a in LowerCone S )
assume that
A1: a in S and
A2: a in LowerCone S ; ::_thesis: contradiction
 ex a1 being Element of A st
( a1 = a & ( for a2 being Element of A st a2 in S holds
a1 < a2 ) ) by A2;
hence  contradiction by A1; ::_thesis: verum
end;

theorem Th21: :: ORDERS_2:21
for A being non empty Poset
for a being Element of A holds not a in LowerCone {a}
proof
let A be non empty Poset; ::_thesis: for a being Element of A holds not a in LowerCone {a}
let a be Element of A; ::_thesis: not a in LowerCone {a}
 a in {a} by TARSKI:def_1;
hence  not a in LowerCone {a} by Th20; ::_thesis: verum
end;

theorem :: ORDERS_2:22
for A being non empty Poset
for c, a being Element of A holds
( c < a iff a in UpperCone {c} )
proof
let A be non empty Poset; ::_thesis: for c, a being Element of A holds
( c < a iff a in UpperCone {c} )
let c, a be Element of A; ::_thesis: ( c < a iff a in UpperCone {c} )
thus  ( c < a implies a in UpperCone {c} ) ::_thesis: ( a in UpperCone {c} implies c < a )
proof
assume  c < a ; ::_thesis: a in UpperCone {c}
then  for b being Element of A st b in {c} holds
b < a by TARSKI:def_1;
hence  a in UpperCone {c} ; ::_thesis: verum
end;
assume  a in UpperCone {c} ; ::_thesis: c < a
then A1: ex a1 being Element of A st
( a1 = a & ( for a2 being Element of A st a2 in {c} holds
a2 < a1 ) ) ;
 c in {c} by TARSKI:def_1;
hence  c < a by A1; ::_thesis: verum
end;

theorem Th23: :: ORDERS_2:23
for A being non empty Poset
for a, c being Element of A holds
( a < c iff a in LowerCone {c} )
proof
let A be non empty Poset; ::_thesis: for a, c being Element of A holds
( a < c iff a in LowerCone {c} )
let a, c be Element of A; ::_thesis: ( a < c iff a in LowerCone {c} )
thus  ( a < c implies a in LowerCone {c} ) ::_thesis: ( a in LowerCone {c} implies a < c )
proof
assume  a < c ; ::_thesis: a in LowerCone {c}
then  for b being Element of A st b in {c} holds
a < b by TARSKI:def_1;
hence  a in LowerCone {c} ; ::_thesis: verum
end;
assume  a in LowerCone {c} ; ::_thesis: a < c
then A1: ex a1 being Element of A st
( a1 = a & ( for a2 being Element of A st a2 in {c} holds
a1 < a2 ) ) ;
 c in {c} by TARSKI:def_1;
hence  a < c by A1; ::_thesis: verum
end;

definition
let A be non empty Poset;
let S be Subset of A;
let a be Element of A;
func InitSegm (S,a) ->  Subset of A equals :: ORDERS_2:def 10
(LowerCone {a}) /\ S;
correctness
coherence
(LowerCone {a}) /\ S is Subset of A;
;
end;

:: deftheorem  defines InitSegm ORDERS_2:def_10_:_
 for A being non empty Poset
for S being Subset of A
for a being Element of A holds InitSegm (S,a) = (LowerCone {a}) /\ S;

definition
let A be non empty Poset;
let S be Subset of A;
mode Initial_Segm of S ->  Subset of A means :Def11: :: ORDERS_2:def 11
 ex a being Element of A st
( a in S & it = InitSegm (S,a) ) if S <> {}
otherwise it = {} ;
existence
 ( ( S <> {} implies ex b1 being Subset of A ex a being Element of A st
( a in S & b1 = InitSegm (S,a) ) ) & ( not S <> {} implies ex b1 being Subset of A st b1 = {} ) )
proof
now__::_thesis:_(_S_<>_{}_implies_ex_T_being_Subset_of_A_st_
(_(_S_<>_{}_implies_ex_a_being_Element_of_A_st_
(_a_in_S_&_T_=_InitSegm_(S,a)_)_)_&_(_S_=_{}_implies_T_=_{}_)_)_)
set x = the Element of S;
assume  S <> {} ; ::_thesis: ex T being Subset of A st
( ( S <> {} implies ex a being Element of A st
( a in S & T = InitSegm (S,a) ) ) & ( S = {} implies T = {} ) )
then reconsider x = the Element of S as Element of A by Lm1;
take T = InitSegm (S,x); ::_thesis: ( ( S <> {} implies ex a being Element of A st
( a in S & T = InitSegm (S,a) ) ) & ( S = {} implies T = {} ) )
thus  ( S <> {} implies ex a being Element of A st
( a in S & T = InitSegm (S,a) ) ) ; ::_thesis: ( S = {} implies T = {} )
thus  ( S = {} implies T = {} ) ; ::_thesis: verum
end;
hence  ( ( S <> {} implies ex b1 being Subset of A ex a being Element of A st
( a in S & b1 = InitSegm (S,a) ) ) & ( not S <> {} implies ex b1 being Subset of A st b1 = {} ) ) ; ::_thesis: verum
end;
consistency
 for b1 being Subset of A holds verum ;
end;

:: deftheorem Def11 defines Initial_Segm ORDERS_2:def_11_:_
 for A being non empty Poset
for S, b3 being Subset of A holds
( ( S <> {} implies ( b3 is Initial_Segm of S iff ex a being Element of A st
( a in S & b3 = InitSegm (S,a) ) ) ) & ( not S <> {} implies ( b3 is Initial_Segm of S iff b3 = {} ) ) );

theorem Th24: :: ORDERS_2:24
for A being non empty Poset
for a, b being Element of A
for S being Subset of A holds
( a in InitSegm (S,b) iff ( a < b & a in S ) )
proof
let A be non empty Poset; ::_thesis: for a, b being Element of A
for S being Subset of A holds
( a in InitSegm (S,b) iff ( a < b & a in S ) )
let a, b be Element of A; ::_thesis: for S being Subset of A holds
( a in InitSegm (S,b) iff ( a < b & a in S ) )
let S be Subset of A; ::_thesis: ( a in InitSegm (S,b) iff ( a < b & a in S ) )
 ( a in InitSegm (S,b) iff ( a in LowerCone {b} & a in S ) ) by XBOOLE_0:def_4;
hence  ( a in InitSegm (S,b) iff ( a < b & a in S ) ) by Th23; ::_thesis: verum
end;

theorem :: ORDERS_2:25
for A being non empty Poset
for a being Element of A holds InitSegm (({} A),a) = {} ;

theorem Th26: :: ORDERS_2:26
for A being non empty Poset
for a being Element of A
for S being Subset of A holds not a in InitSegm (S,a)
proof
let A be non empty Poset; ::_thesis: for a being Element of A
for S being Subset of A holds not a in InitSegm (S,a)
let a be Element of A; ::_thesis: for S being Subset of A holds not a in InitSegm (S,a)
let S be Subset of A; ::_thesis: not a in InitSegm (S,a)
assume  a in InitSegm (S,a) ; ::_thesis: contradiction
then  a in LowerCone {a} by XBOOLE_0:def_4;
then A1: ex a1 being Element of A st
( a = a1 & ( for a2 being Element of A st a2 in {a} holds
a1 < a2 ) ) ;
 a in {a} by TARSKI:def_1;
hence  contradiction by A1; ::_thesis: verum
end;

theorem :: ORDERS_2:27
for A being non empty Poset
for a1, a2 being Element of A
for S being Subset of A st a1 < a2 holds
InitSegm (S,a1) c= InitSegm (S,a2)
proof
let A be non empty Poset; ::_thesis: for a1, a2 being Element of A
for S being Subset of A st a1 < a2 holds
InitSegm (S,a1) c= InitSegm (S,a2)
let a1, a2 be Element of A; ::_thesis: for S being Subset of A st a1 < a2 holds
InitSegm (S,a1) c= InitSegm (S,a2)
let S be Subset of A; ::_thesis: ( a1 < a2 implies InitSegm (S,a1) c= InitSegm (S,a2) )
assume A1: a1 < a2 ; ::_thesis: InitSegm (S,a1) c= InitSegm (S,a2)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in InitSegm (S,a1) or x in InitSegm (S,a2) )
assume A2: x in InitSegm (S,a1) ; ::_thesis: x in InitSegm (S,a2)
then  x in LowerCone {a1} by XBOOLE_0:def_4;
then consider a being Element of A such that
A3: a = x and
A4: for b being Element of A st b in {a1} holds
a < b ;
 a1 in {a1} by TARSKI:def_1;
then  a < a1 by A4;
then  a < a2 by A1, Th5;
then  for b being Element of A st b in {a2} holds
a < b by TARSKI:def_1;
then A5: x in LowerCone {a2} by A3;
 x in S by A2, XBOOLE_0:def_4;
hence  x in InitSegm (S,a2) by A5, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem Th28: :: ORDERS_2:28
for A being non empty Poset
for a being Element of A
for S, T being Subset of A st S c= T holds
InitSegm (S,a) c= InitSegm (T,a)
proof
let A be non empty Poset; ::_thesis: for a being Element of A
for S, T being Subset of A st S c= T holds
InitSegm (S,a) c= InitSegm (T,a)
let a be Element of A; ::_thesis: for S, T being Subset of A st S c= T holds
InitSegm (S,a) c= InitSegm (T,a)
let S, T be Subset of A; ::_thesis: ( S c= T implies InitSegm (S,a) c= InitSegm (T,a) )
assume A1: S c= T ; ::_thesis: InitSegm (S,a) c= InitSegm (T,a)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in InitSegm (S,a) or x in InitSegm (T,a) )
assume  x in InitSegm (S,a) ; ::_thesis: x in InitSegm (T,a)
then  ( x in S & x in LowerCone {a} ) by XBOOLE_0:def_4;
hence  x in InitSegm (T,a) by A1, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem Th29: :: ORDERS_2:29
for A being non empty Poset
for S being Subset of A
for I being Initial_Segm of S holds I c= S
proof
let A be non empty Poset; ::_thesis: for S being Subset of A
for I being Initial_Segm of S holds I c= S
let S be Subset of A; ::_thesis: for I being Initial_Segm of S holds I c= S
let I be Initial_Segm of S; ::_thesis: I c= S
percases ( S = {} or S <> {} ) ;
suppose S = {} ; ::_thesis: I c= S
hence  I c= S by Def11; ::_thesis: verum
end;
suppose S <> {} ; ::_thesis: I c= S
then  ex a being Element of A st
( a in S & I = InitSegm (S,a) ) by Def11;
hence  I c= S by XBOOLE_1:17; ::_thesis: verum
end;
end;
end;

theorem Th30: :: ORDERS_2:30
for A being non empty Poset
for S being Subset of A holds
( S <> {} iff not S is Initial_Segm of S )
proof
let A be non empty Poset; ::_thesis: for S being Subset of A holds
( S <> {} iff not S is Initial_Segm of S )
let S be Subset of A; ::_thesis: ( S <> {} iff not S is Initial_Segm of S )
thus  ( S <> {} implies not S is Initial_Segm of S ) ::_thesis: ( S is not Initial_Segm of S implies S <> {} )
proof
assume  ( S <> {} & S is Initial_Segm of S ) ; ::_thesis: contradiction
then consider a being Element of A such that
A1: ( a in S & S = InitSegm (S,a) ) by Def11;
 a in LowerCone {a} by A1, XBOOLE_0:def_4;
hence  contradiction by Th21; ::_thesis: verum
end;
thus  ( S is not Initial_Segm of S implies S <> {} ) by Def11; ::_thesis: verum
end;

theorem Th31: :: ORDERS_2:31
for A being non empty Poset
for S, T being Subset of A st S <> {} & S is Initial_Segm of T holds
not T is Initial_Segm of S
proof
let A be non empty Poset; ::_thesis: for S, T being Subset of A st S <> {} & S is Initial_Segm of T holds
not T is Initial_Segm of S
let S, T be Subset of A; ::_thesis: ( S <> {} & S is Initial_Segm of T implies not T is Initial_Segm of S )
assume that
A1: S <> {} and
A2: S is Initial_Segm of T and
A3: T is Initial_Segm of S ; ::_thesis: contradiction
now__::_thesis:_contradiction
percases ( S = {} or T = {} or ( S <> {} & T <> {} ) ) ;
suppose S = {} ; ::_thesis: contradiction
hence  contradiction by A1; ::_thesis: verum
end;
suppose T = {} ; ::_thesis: contradiction
hence  contradiction by A1, A2, Def11; ::_thesis: verum
end;
supposeA4: ( S <> {} & T <> {} ) ; ::_thesis: contradiction
then consider a2 being Element of A such that
A5: a2 in T and
A6: S = InitSegm (T,a2) by A2, Def11;
consider a1 being Element of A such that
A7: a1 in S and
A8: T = InitSegm (S,a1) by A3, A4, Def11;
 a1 in LowerCone {a2} by A7, A6, XBOOLE_0:def_4;
then A9: ex a being Element of A st
( a = a1 & ( for b being Element of A st b in {a2} holds
a < b ) ) ;
 a2 in LowerCone {a1} by A8, A5, XBOOLE_0:def_4;
then A10: ex a3 being Element of A st
( a3 = a2 & ( for b being Element of A st b in {a1} holds
a3 < b ) ) ;
 a1 in {a1} by TARSKI:def_1;
then A11: a2 < a1 by A10;
 a2 in {a2} by TARSKI:def_1;
then  a1 < a2 by A9;
hence  contradiction by A11, Th4; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;

theorem Th32: :: ORDERS_2:32
for A being non empty Poset
for a1, a2 being Element of A
for S, T being Subset of A st a1 < a2 & a1 in S & a2 in T & T is Initial_Segm of S holds
a1 in T
proof
let A be non empty Poset; ::_thesis: for a1, a2 being Element of A
for S, T being Subset of A st a1 < a2 & a1 in S & a2 in T & T is Initial_Segm of S holds
a1 in T
let a1, a2 be Element of A; ::_thesis: for S, T being Subset of A st a1 < a2 & a1 in S & a2 in T & T is Initial_Segm of S holds
a1 in T
let S, T be Subset of A; ::_thesis: ( a1 < a2 & a1 in S & a2 in T & T is Initial_Segm of S implies a1 in T )
assume that
A1: a1 < a2 and
A2: a1 in S and
A3: a2 in T and
A4: T is Initial_Segm of S ; ::_thesis: a1 in T
consider a being Element of A such that
 a in S and
A5: T = InitSegm (S,a) by A2, A4, Def11;
now__::_thesis:_for_b_being_Element_of_A_st_b_in_{a}_holds_
a1_<_b
let b be Element of A; ::_thesis: ( b in {a} implies a1 < b )
assume  b in {a} ; ::_thesis: a1 < b
then A6: b = a by TARSKI:def_1;
 a2 in LowerCone {a} by A3, A5, XBOOLE_0:def_4;
then A7: ex a3 being Element of A st
( a3 = a2 & ( for c being Element of A st c in {a} holds
a3 < c ) ) ;
 a in {a} by TARSKI:def_1;
then  a2 < a by A7;
hence  a1 < b by A1, A6, Th5; ::_thesis: verum
end;
then  a1 in LowerCone {a} ;
hence  a1 in T by A2, A5, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem Th33: :: ORDERS_2:33
for A being non empty Poset
for a being Element of A
for S, T being Subset of A st a in S & S is Initial_Segm of T holds
InitSegm (S,a) = InitSegm (T,a)
proof
let A be non empty Poset; ::_thesis: for a being Element of A
for S, T being Subset of A st a in S & S is Initial_Segm of T holds
InitSegm (S,a) = InitSegm (T,a)
let a be Element of A; ::_thesis: for S, T being Subset of A st a in S & S is Initial_Segm of T holds
InitSegm (S,a) = InitSegm (T,a)
let S, T be Subset of A; ::_thesis: ( a in S & S is Initial_Segm of T implies InitSegm (S,a) = InitSegm (T,a) )
assume that
A1: a in S and
A2: S is Initial_Segm of T ; ::_thesis: InitSegm (S,a) = InitSegm (T,a)
A3: S c= T by A2, Th29;
thus  InitSegm (S,a) c= InitSegm (T,a) :: according to XBOOLE_0:def_10 ::_thesis: InitSegm (T,a) c= InitSegm (S,a)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in InitSegm (S,a) or x in InitSegm (T,a) )
assume  x in InitSegm (S,a) ; ::_thesis: x in InitSegm (T,a)
then  ( x in LowerCone {a} & x in S ) by XBOOLE_0:def_4;
hence  x in InitSegm (T,a) by A3, XBOOLE_0:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in InitSegm (T,a) or x in InitSegm (S,a) )
assume A4: x in InitSegm (T,a) ; ::_thesis: x in InitSegm (S,a)
then A5: x in LowerCone {a} by XBOOLE_0:def_4;
then consider a1 being Element of A such that
A6: x = a1 and
A7: for a2 being Element of A st a2 in {a} holds
a1 < a2 ;
A8: a1 in T by A4, A6, XBOOLE_0:def_4;
 a in {a} by TARSKI:def_1;
then  a1 < a by A7;
then  x in S by A1, A2, A6, A8, Th32;
hence  x in InitSegm (S,a) by A5, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem :: ORDERS_2:34
for A being non empty Poset
for S, T being Subset of A st S c= T & the InternalRel of A well_orders T & ( for a1, a2 being Element of A st a2 in S & a1 < a2 holds
a1 in S ) & not S = T holds
S is Initial_Segm of T
proof
let A be non empty Poset; ::_thesis: for S, T being Subset of A st S c= T & the InternalRel of A well_orders T & ( for a1, a2 being Element of A st a2 in S & a1 < a2 holds
a1 in S ) & not S = T holds
S is Initial_Segm of T
let S, T be Subset of A; ::_thesis: ( S c= T & the InternalRel of A well_orders T & ( for a1, a2 being Element of A st a2 in S & a1 < a2 holds
a1 in S ) & not S = T implies S is Initial_Segm of T )
assume that
A1: S c= T and
A2: the InternalRel of A well_orders T and
A3: for a1, a2 being Element of A st a2 in S & a1 < a2 holds
a1 in S and
A4: S <> T ; ::_thesis: S is Initial_Segm of T
percases ( T <> {} or T = {} ) ;
:: according to ORDERS_2:def_11
case T <> {} ; ::_thesis: ex a being Element of A st
( a in T & S = InitSegm (T,a) )
set Y = T \ S;
 not T c= S by A1, A4, XBOOLE_0:def_10;
then  T \ S <> {} by XBOOLE_1:37;
then consider x being set  such that
A5: x in T \ S and
A6: for y being set st y in T \ S holds
[x,y] in the InternalRel of A by A2, WELLORD1:5, XBOOLE_1:36;
reconsider x = x as Element of A by A5;
take  x ; ::_thesis: ( x in T & S = InitSegm (T,x) )
thus A7: x in T by A5, XBOOLE_0:def_5; ::_thesis: S = InitSegm (T,x)
 S = (LowerCone {x}) /\ T
proof
thus  S c= (LowerCone {x}) /\ T :: according to XBOOLE_0:def_10 ::_thesis: (LowerCone {x}) /\ T c= S
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in S or y in (LowerCone {x}) /\ T )
assume A8: y in S ; ::_thesis: y in (LowerCone {x}) /\ T
then reconsider a = y as Element of A ;
now__::_thesis:_for_a1_being_Element_of_A_st_a1_in_{x}_holds_
a_<_a1
let a1 be Element of A; ::_thesis: ( a1 in {x} implies a < a1 )
assume that
A9: a1 in {x} and
A10: not a < a1 ; ::_thesis: contradiction
A11: a1 = x by A9, TARSKI:def_1;
then A12: a1 <> a by A5, A8, XBOOLE_0:def_5;
 T is Chain of A by A2, Th13;
then  a1 <= a by A1, A7, A8, A10, A11, Th12;
then  a1 < a by A12, Def6;
then  a1 in S by A3, A8;
hence  contradiction by A5, A11, XBOOLE_0:def_5; ::_thesis: verum
end;
then  y in  {  a1 where a1 is Element of A : for a2 being Element of A st a2 in {x} holds
a1 < a2  }  ;
hence  y in (LowerCone {x}) /\ T by A1, A8, XBOOLE_0:def_4; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (LowerCone {x}) /\ T or y in S )
assume A13: y in (LowerCone {x}) /\ T ; ::_thesis: y in S
then  y in LowerCone {x} by XBOOLE_0:def_4;
then consider a being Element of A such that
A14: a = y and
A15: for a2 being Element of A st a2 in {x} holds
a < a2 ;
A16: now__::_thesis:_not_y_in_T_\_S
assume  y in T \ S ; ::_thesis: contradiction
then  [x,y] in the InternalRel of A by A6;
then A17: x <= a by A14, Def5;
 x in {x} by TARSKI:def_1;
hence  contradiction by A15, A17, Th6; ::_thesis: verum
end;
 y in T by A13, XBOOLE_0:def_4;
hence  y in S by A16, XBOOLE_0:def_5; ::_thesis: verum
end;
hence  S = InitSegm (T,x) ; ::_thesis: verum
end;
case T = {} ; ::_thesis: S = {}
hence  S = {} by A1; ::_thesis: verum
end;
end;
end;

theorem Th35: :: ORDERS_2:35
for A being non empty Poset
for S, T being Subset of A st S c= T & the InternalRel of A well_orders T & ( for a1, a2 being Element of A st a2 in S & a1 in T & a1 < a2 holds
a1 in S ) & not S = T holds
S is Initial_Segm of T
proof
let A be non empty Poset; ::_thesis: for S, T being Subset of A st S c= T & the InternalRel of A well_orders T & ( for a1, a2 being Element of A st a2 in S & a1 in T & a1 < a2 holds
a1 in S ) & not S = T holds
S is Initial_Segm of T
let S, T be Subset of A; ::_thesis: ( S c= T & the InternalRel of A well_orders T & ( for a1, a2 being Element of A st a2 in S & a1 in T & a1 < a2 holds
a1 in S ) & not S = T implies S is Initial_Segm of T )
assume that
A1: S c= T and
A2: the InternalRel of A well_orders T and
A3: for a1, a2 being Element of A st a2 in S & a1 in T & a1 < a2 holds
a1 in S and
A4: S <> T ; ::_thesis: S is Initial_Segm of T
percases ( T <> {} or T = {} ) ;
:: according to ORDERS_2:def_11
case T <> {} ; ::_thesis: ex a being Element of A st
( a in T & S = InitSegm (T,a) )
set Y = T \ S;
 not T c= S by A1, A4, XBOOLE_0:def_10;
then  T \ S <> {} by XBOOLE_1:37;
then consider x being set  such that
A5: x in T \ S and
A6: for y being set st y in T \ S holds
[x,y] in the InternalRel of A by A2, WELLORD1:5, XBOOLE_1:36;
reconsider x = x as Element of A by A5;
take  x ; ::_thesis: ( x in T & S = InitSegm (T,x) )
thus A7: x in T by A5, XBOOLE_0:def_5; ::_thesis: S = InitSegm (T,x)
 S = (LowerCone {x}) /\ T
proof
thus  S c= (LowerCone {x}) /\ T :: according to XBOOLE_0:def_10 ::_thesis: (LowerCone {x}) /\ T c= S
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in S or y in (LowerCone {x}) /\ T )
assume A8: y in S ; ::_thesis: y in (LowerCone {x}) /\ T
then reconsider a = y as Element of A ;
now__::_thesis:_for_a1_being_Element_of_A_st_a1_in_{x}_holds_
a_<_a1
let a1 be Element of A; ::_thesis: ( a1 in {x} implies a < a1 )
assume that
A9: a1 in {x} and
A10: not a < a1 ; ::_thesis: contradiction
A11: a1 = x by A9, TARSKI:def_1;
then A12: a1 <> a by A5, A8, XBOOLE_0:def_5;
 T is Chain of A by A2, Th13;
then  a1 <= a by A1, A7, A8, A10, A11, Th12;
then  a1 < a by A12, Def6;
then  a1 in S by A3, A7, A8, A11;
hence  contradiction by A5, A11, XBOOLE_0:def_5; ::_thesis: verum
end;
then  y in  {  a1 where a1 is Element of A : for a2 being Element of A st a2 in {x} holds
a1 < a2  }  ;
hence  y in (LowerCone {x}) /\ T by A1, A8, XBOOLE_0:def_4; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (LowerCone {x}) /\ T or y in S )
assume A13: y in (LowerCone {x}) /\ T ; ::_thesis: y in S
then  y in LowerCone {x} by XBOOLE_0:def_4;
then consider a being Element of A such that
A14: a = y and
A15: for a2 being Element of A st a2 in {x} holds
a < a2 ;
A16: now__::_thesis:_not_y_in_T_\_S
assume  y in T \ S ; ::_thesis: contradiction
then  [x,y] in the InternalRel of A by A6;
then A17: x <= a by A14, Def5;
 x in {x} by TARSKI:def_1;
hence  contradiction by A15, A17, Th6; ::_thesis: verum
end;
 y in T by A13, XBOOLE_0:def_4;
hence  y in S by A16, XBOOLE_0:def_5; ::_thesis: verum
end;
hence  S = InitSegm (T,x) ; ::_thesis: verum
end;
case T = {} ; ::_thesis: S = {}
hence  S = {} by A1; ::_thesis: verum
end;
end;
end;

definition
let A be non empty Poset;
let f be Choice_Function of BOOL the carrier of A;
mode Chain of f ->  Chain of A means :Def12: :: ORDERS_2:def 12
( it <> {} & the InternalRel of A well_orders it & ( for a being Element of A st a in it holds
f . (UpperCone (InitSegm (it,a))) = a ) );
existence
 ex b1 being Chain of A st
( b1 <> {} & the InternalRel of A well_orders b1 & ( for a being Element of A st a in b1 holds
f . (UpperCone (InitSegm (b1,a))) = a ) )
proof
set AC = the carrier of A;
 ( the carrier of A in BOOL the carrier of A & not {} in BOOL the carrier of A ) by ORDERS_1:1, ORDERS_1:2;
then reconsider aa = f . the carrier of A as Element of A by ORDERS_1:def_1;
reconsider X = {aa} as Chain of A by Th8;
take  X ; ::_thesis: ( X <> {} & the InternalRel of A well_orders X & ( for a being Element of A st a in X holds
f . (UpperCone (InitSegm (X,a))) = a ) )
thus  X <> {} ; ::_thesis: ( the InternalRel of A well_orders X & ( for a being Element of A st a in X holds
f . (UpperCone (InitSegm (X,a))) = a ) )
A1: the InternalRel of A is_antisymmetric_in the carrier of A by Def4;
 ( the InternalRel of A is_reflexive_in the carrier of A & the InternalRel of A is_transitive_in the carrier of A ) by Def2, Def3;
hence  ( the InternalRel of A is_reflexive_in X & the InternalRel of A is_transitive_in X & the InternalRel of A is_antisymmetric_in X ) by A1, ORDERS_1:8, ORDERS_1:9, ORDERS_1:10; :: according to WELLORD1:def_5 ::_thesis: ( the InternalRel of A is_connected_in X & the InternalRel of A is_well_founded_in X & ( for a being Element of A st a in X holds
f . (UpperCone (InitSegm (X,a))) = a ) )
 the InternalRel of A is_strongly_connected_in X by Def7;
hence  the InternalRel of A is_connected_in X by ORDERS_1:7; ::_thesis: ( the InternalRel of A is_well_founded_in X & ( for a being Element of A st a in X holds
f . (UpperCone (InitSegm (X,a))) = a ) )
thus  the InternalRel of A is_well_founded_in X ::_thesis: for a being Element of A st a in X holds
f . (UpperCone (InitSegm (X,a))) = a
proof
reconsider x = aa as set ;
let Y be set ; :: according to WELLORD1:def_3 ::_thesis: ( not Y c= X or Y = {} or ex b1 being set st
( b1 in Y & the InternalRel of A -Seg b1 misses Y ) )
assume that
A2: Y c= X and
A3: Y <> {} ; ::_thesis: ex b1 being set st
( b1 in Y & the InternalRel of A -Seg b1 misses Y )
take  x ; ::_thesis: ( x in Y & the InternalRel of A -Seg x misses Y )
 Y = X by A2, A3, ZFMISC_1:33;
hence  x in Y by TARSKI:def_1; ::_thesis: the InternalRel of A -Seg x misses Y
thus  ( the InternalRel of A -Seg x) /\ Y c= {} :: according to XBOOLE_0:def_7,XBOOLE_0:def_10 ::_thesis: {} c= ( the InternalRel of A -Seg x) /\ Y
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in ( the InternalRel of A -Seg x) /\ Y or y in {} )
assume A4: y in ( the InternalRel of A -Seg x) /\ Y ; ::_thesis: y in {}
then  y in Y by XBOOLE_0:def_4;
then A5: y = aa by A2, TARSKI:def_1;
 y in the InternalRel of A -Seg x by A4, XBOOLE_0:def_4;
hence  y in {} by A5, WELLORD1:1; ::_thesis: verum
end;
thus  {} c= ( the InternalRel of A -Seg x) /\ Y by XBOOLE_1:2; ::_thesis: verum
end;
let a be Element of A; ::_thesis: ( a in X implies f . (UpperCone (InitSegm (X,a))) = a )
assume  a in X ; ::_thesis: f . (UpperCone (InitSegm (X,a))) = a
then A6: a = aa by TARSKI:def_1;
 (LowerCone {a}) /\ X c= {} A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (LowerCone {a}) /\ X or x in {} A )
assume A7: x in (LowerCone {a}) /\ X ; ::_thesis: x in {} A
then  x in LowerCone {a} by XBOOLE_0:def_4;
then A8: ex a1 being Element of A st
( x = a1 & ( for a2 being Element of A st a2 in {a} holds
a1 < a2 ) ) ;
 x in X by A7, XBOOLE_0:def_4;
hence  x in {} A by A6, A8; ::_thesis: verum
end;
then  (LowerCone {a}) /\ X = {} A ;
hence  f . (UpperCone (InitSegm (X,a))) = a by A6, Th14; ::_thesis: verum
end;
end;

:: deftheorem Def12 defines Chain ORDERS_2:def_12_:_
 for A being non empty Poset
for f being Choice_Function of BOOL the carrier of A
for b3 being Chain of A holds
( b3 is Chain of f iff ( b3 <> {} & the InternalRel of A well_orders b3 & ( for a being Element of A st a in b3 holds
f . (UpperCone (InitSegm (b3,a))) = a ) ) );


theorem Th36: :: ORDERS_2:36
for A being non empty Poset
for f being Choice_Function of BOOL the carrier of A holds {(f . the carrier of A)} is Chain of f
proof
let A be non empty Poset; ::_thesis: for f being Choice_Function of BOOL the carrier of A holds {(f . the carrier of A)} is Chain of f
let f be Choice_Function of BOOL the carrier of A; ::_thesis: {(f . the carrier of A)} is Chain of f
set AC = the carrier of A;
 ( the carrier of A in BOOL the carrier of A & not {} in BOOL the carrier of A ) by ORDERS_1:1, ORDERS_1:2;
then reconsider aa = f . the carrier of A as Element of A by ORDERS_1:def_1;
reconsider X = {aa} as Chain of A by Th8;
A1: the InternalRel of A is_well_founded_in X
proof
reconsider x = aa as set ;
let Y be set ; :: according to WELLORD1:def_3 ::_thesis: ( not Y c= X or Y = {} or ex b1 being set st
( b1 in Y & the InternalRel of A -Seg b1 misses Y ) )
assume that
A2: Y c= X and
A3: Y <> {} ; ::_thesis: ex b1 being set st
( b1 in Y & the InternalRel of A -Seg b1 misses Y )
take  x ; ::_thesis: ( x in Y & the InternalRel of A -Seg x misses Y )
 Y = X by A2, A3, ZFMISC_1:33;
hence  x in Y by TARSKI:def_1; ::_thesis: the InternalRel of A -Seg x misses Y
thus  ( the InternalRel of A -Seg x) /\ Y c= {} :: according to XBOOLE_0:def_7,XBOOLE_0:def_10 ::_thesis: {} c= ( the InternalRel of A -Seg x) /\ Y
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in ( the InternalRel of A -Seg x) /\ Y or y in {} )
assume A4: y in ( the InternalRel of A -Seg x) /\ Y ; ::_thesis: y in {}
then  y in Y by XBOOLE_0:def_4;
then A5: y = aa by A2, TARSKI:def_1;
 y in the InternalRel of A -Seg x by A4, XBOOLE_0:def_4;
hence  y in {} by A5, WELLORD1:1; ::_thesis: verum
end;
thus  {} c= ( the InternalRel of A -Seg x) /\ Y by XBOOLE_1:2; ::_thesis: verum
end;
A6: for a being Element of A st a in X holds
f . (UpperCone (InitSegm (X,a))) = a
proof
let a be Element of A; ::_thesis: ( a in X implies f . (UpperCone (InitSegm (X,a))) = a )
assume  a in X ; ::_thesis: f . (UpperCone (InitSegm (X,a))) = a
then A7: a = aa by TARSKI:def_1;
 (LowerCone {a}) /\ X c= {} A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (LowerCone {a}) /\ X or x in {} A )
assume A8: x in (LowerCone {a}) /\ X ; ::_thesis: x in {} A
then  x in LowerCone {a} by XBOOLE_0:def_4;
then A9: ex a1 being Element of A st
( x = a1 & ( for a2 being Element of A st a2 in {a} holds
a1 < a2 ) ) ;
 x in X by A8, XBOOLE_0:def_4;
hence  x in {} A by A7, A9; ::_thesis: verum
end;
then  (LowerCone {a}) /\ X = {} A ;
hence  f . (UpperCone (InitSegm (X,a))) = a by A7, Th14; ::_thesis: verum
end;
 the InternalRel of A is_strongly_connected_in X by Def7;
then A10: the InternalRel of A is_connected_in X by ORDERS_1:7;
 the InternalRel of A is_antisymmetric_in the carrier of A by Def4;
then A11: the InternalRel of A is_antisymmetric_in X by ORDERS_1:9;
 the InternalRel of A is_transitive_in the carrier of A by Def3;
then A12: the InternalRel of A is_transitive_in X by ORDERS_1:10;
 the InternalRel of A is_reflexive_in the carrier of A by Def2;
then  the InternalRel of A is_reflexive_in X by ORDERS_1:8;
then  the InternalRel of A well_orders X by A12, A11, A10, A1, WELLORD1:def_5;
hence  {(f . the carrier of A)} is Chain of f by A6, Def12; ::_thesis: verum
end;

theorem Th37: :: ORDERS_2:37
for A being non empty Poset
for f being Choice_Function of BOOL the carrier of A
for fC being Chain of f holds f . the carrier of A in fC
proof
let A be non empty Poset; ::_thesis: for f being Choice_Function of BOOL the carrier of A
for fC being Chain of f holds f . the carrier of A in fC
let f be Choice_Function of BOOL the carrier of A; ::_thesis: for fC being Chain of f holds f . the carrier of A in fC
let fC be Chain of f; ::_thesis: f . the carrier of A in fC
 ( the InternalRel of A well_orders fC & fC <> {} ) by Def12;
then consider x being set  such that
A1: x in fC and
A2: for y being set st y in fC holds
[x,y] in the InternalRel of A by WELLORD1:5;
reconsider x = x as Element of A by A1;
A3: now__::_thesis:_not_(LowerCone_{x})_/\_fC_<>_{}_A
set y = the Element of (LowerCone {x}) /\ fC;
assume A4: (LowerCone {x}) /\ fC <> {} A ; ::_thesis: contradiction
then reconsider a = the Element of (LowerCone {x}) /\ fC as Element of A by Lm1;
 a in LowerCone {x} by A4, XBOOLE_0:def_4;
then A5: ex a1 being Element of A st
( a = a1 & ( for a2 being Element of A st a2 in {x} holds
a1 < a2 ) ) ;
 the Element of (LowerCone {x}) /\ fC in fC by A4, XBOOLE_0:def_4;
then  [x, the Element of (LowerCone {x}) /\ fC] in the InternalRel of A by A2;
then A6: x <= a by Def5;
 x in {x} by TARSKI:def_1;
hence  contradiction by A6, A5, Th6; ::_thesis: verum
end;
 (LowerCone {x}) /\ fC = InitSegm (fC,x) ;
then  f . (UpperCone ((LowerCone {x}) /\ fC)) = x by A1, Def12;
hence  f . the carrier of A in fC by A1, A3, Th14; ::_thesis: verum
end;

theorem Th38: :: ORDERS_2:38
for A being non empty Poset
for a, b being Element of A
for f being Choice_Function of BOOL the carrier of A
for fC being Chain of f st a in fC & b = f . the carrier of A holds
b <= a
proof
let A be non empty Poset; ::_thesis: for a, b being Element of A
for f being Choice_Function of BOOL the carrier of A
for fC being Chain of f st a in fC & b = f . the carrier of A holds
b <= a
let a, b be Element of A; ::_thesis: for f being Choice_Function of BOOL the carrier of A
for fC being Chain of f st a in fC & b = f . the carrier of A holds
b <= a
let f be Choice_Function of BOOL the carrier of A; ::_thesis: for fC being Chain of f st a in fC & b = f . the carrier of A holds
b <= a
let fC be Chain of f; ::_thesis: ( a in fC & b = f . the carrier of A implies b <= a )
assume that
A1: a in fC and
A2: b = f . the carrier of A ; ::_thesis: b <= a
 ( the InternalRel of A well_orders fC & fC <> {} ) by Def12;
then consider x being set  such that
A3: x in fC and
A4: for y being set st y in fC holds
[x,y] in the InternalRel of A by WELLORD1:5;
reconsider x = x as Element of A by A3;
A5: now__::_thesis:_not_(LowerCone_{x})_/\_fC_<>_{}_A
set y = the Element of (LowerCone {x}) /\ fC;
assume A6: (LowerCone {x}) /\ fC <> {} A ; ::_thesis: contradiction
then reconsider a = the Element of (LowerCone {x}) /\ fC as Element of A by Lm1;
 a in LowerCone {x} by A6, XBOOLE_0:def_4;
then A7: ex a1 being Element of A st
( a = a1 & ( for a2 being Element of A st a2 in {x} holds
a1 < a2 ) ) ;
 the Element of (LowerCone {x}) /\ fC in fC by A6, XBOOLE_0:def_4;
then  [x, the Element of (LowerCone {x}) /\ fC] in the InternalRel of A by A4;
then A8: x <= a by Def5;
 x in {x} by TARSKI:def_1;
hence  contradiction by A8, A7, Th6; ::_thesis: verum
end;
 (LowerCone {x}) /\ fC = InitSegm (fC,x) ;
then  f . (UpperCone ((LowerCone {x}) /\ fC)) = x by A3, Def12;
then A9: f . the carrier of A = x by A5, Th14;
 [x,a] in the InternalRel of A by A1, A4;
hence  b <= a by A2, A9, Def5; ::_thesis: verum
end;

theorem :: ORDERS_2:39
for A being non empty Poset
for a being Element of A
for f being Choice_Function of BOOL the carrier of A
for fC being Chain of f st a = f . the carrier of A holds
InitSegm (fC,a) = {}
proof
let A be non empty Poset; ::_thesis: for a being Element of A
for f being Choice_Function of BOOL the carrier of A
for fC being Chain of f st a = f . the carrier of A holds
InitSegm (fC,a) = {}
let a be Element of A; ::_thesis: for f being Choice_Function of BOOL the carrier of A
for fC being Chain of f st a = f . the carrier of A holds
InitSegm (fC,a) = {}
let f be Choice_Function of BOOL the carrier of A; ::_thesis: for fC being Chain of f st a = f . the carrier of A holds
InitSegm (fC,a) = {}
let fC be Chain of f; ::_thesis: ( a = f . the carrier of A implies InitSegm (fC,a) = {} )
set x = the Element of (LowerCone {a}) /\ fC;
assume A1: a = f . the carrier of A ; ::_thesis: InitSegm (fC,a) = {}
then A2: a in fC by Th37;
assume A3: InitSegm (fC,a) <> {} ; ::_thesis: contradiction
then reconsider b = the Element of (LowerCone {a}) /\ fC as Element of A by Lm1;
 the Element of (LowerCone {a}) /\ fC in LowerCone {a} by A3, XBOOLE_0:def_4;
then A4: ex a1 being Element of A st
( a1 = b & ( for a2 being Element of A st a2 in {a} holds
a1 < a2 ) ) ;
 a in {a} by TARSKI:def_1;
then A5: b < a by A4;
A6: the Element of (LowerCone {a}) /\ fC in fC by A3, XBOOLE_0:def_4;
then  a <= b by A1, Th38;
hence  contradiction by A2, A6, A5, Th12; ::_thesis: verum
end;

theorem :: ORDERS_2:40
for A being non empty Poset
for f being Choice_Function of BOOL the carrier of A
for fC1, fC2 being Chain of f holds fC1 meets fC2
proof
let A be non empty Poset; ::_thesis: for f being Choice_Function of BOOL the carrier of A
for fC1, fC2 being Chain of f holds fC1 meets fC2
let f be Choice_Function of BOOL the carrier of A; ::_thesis: for fC1, fC2 being Chain of f holds fC1 meets fC2
let fC1, fC2 be Chain of f; ::_thesis: fC1 meets fC2
 ( f . the carrier of A in fC1 & f . the carrier of A in fC2 ) by Th37;
hence  fC1 meets fC2 by XBOOLE_0:3; ::_thesis: verum
end;

theorem Th41: :: ORDERS_2:41
for A being non empty Poset
for f being Choice_Function of BOOL the carrier of A
for fC1, fC2 being Chain of f st fC1 <> fC2 holds
( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 )
proof
let A be non empty Poset; ::_thesis: for f being Choice_Function of BOOL the carrier of A
for fC1, fC2 being Chain of f st fC1 <> fC2 holds
( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 )
let f be Choice_Function of BOOL the carrier of A; ::_thesis: for fC1, fC2 being Chain of f st fC1 <> fC2 holds
( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 )
let fC1, fC2 be Chain of f; ::_thesis: ( fC1 <> fC2 implies ( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 ) )
assume A1: fC1 <> fC2 ; ::_thesis: ( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 )
set N =  {  a where a is Element of A : ( a in fC1 /\ fC2 & InitSegm (fC1,a) = InitSegm (fC2,a) )  }  ;
A2:  {  a where a is Element of A : ( a in fC1 /\ fC2 & InitSegm (fC1,a) = InitSegm (fC2,a) )  }  c= fC1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  a where a is Element of A : ( a in fC1 /\ fC2 & InitSegm (fC1,a) = InitSegm (fC2,a) )  }  or x in fC1 )
assume  x in  {  a where a is Element of A : ( a in fC1 /\ fC2 & InitSegm (fC1,a) = InitSegm (fC2,a) )  }  ; ::_thesis: x in fC1
then  ex a being Element of A st
( a = x & a in fC1 /\ fC2 & InitSegm (fC1,a) = InitSegm (fC2,a) ) ;
hence  x in fC1 by XBOOLE_0:def_4; ::_thesis: verum
end;
then reconsider N =  {  a where a is Element of A : ( a in fC1 /\ fC2 & InitSegm (fC1,a) = InitSegm (fC2,a) )  }  as Subset of A by XBOOLE_1:1;
A3: N c= fC2
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N or x in fC2 )
assume  x in N ; ::_thesis: x in fC2
then  ex a being Element of A st
( a = x & a in fC1 /\ fC2 & InitSegm (fC1,a) = InitSegm (fC2,a) ) ;
hence  x in fC2 by XBOOLE_0:def_4; ::_thesis: verum
end;
A4: now__::_thesis:_for_a1,_a2_being_Element_of_A_st_a2_in_N_&_a1_in_fC1_&_a1_<_a2_holds_
a1_in_N
let a1, a2 be Element of A; ::_thesis: ( a2 in N & a1 in fC1 & a1 < a2 implies a1 in N )
assume that
A5: a2 in N and
A6: a1 in fC1 and
A7: a1 < a2 ; ::_thesis: a1 in N
A8: ex a being Element of A st
( a = a2 & a in fC1 /\ fC2 & InitSegm (fC1,a) = InitSegm (fC2,a) ) by A5;
A9: InitSegm (fC1,a1) = InitSegm (fC2,a1)
proof
thus  InitSegm (fC1,a1) c= InitSegm (fC2,a1) :: according to XBOOLE_0:def_10 ::_thesis: InitSegm (fC2,a1) c= InitSegm (fC1,a1)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in InitSegm (fC1,a1) or x in InitSegm (fC2,a1) )
assume A10: x in InitSegm (fC1,a1) ; ::_thesis: x in InitSegm (fC2,a1)
then reconsider b = x as Element of A ;
A11: b in fC1 by A10, Th24;
A12: b < a1 by A10, Th24;
then  b < a2 by A7, Th5;
then  b in InitSegm (fC1,a2) by A11, Th24;
then  b in fC2 by A8, Th24;
hence  x in InitSegm (fC2,a1) by A12, Th24; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in InitSegm (fC2,a1) or x in InitSegm (fC1,a1) )
assume A13: x in InitSegm (fC2,a1) ; ::_thesis: x in InitSegm (fC1,a1)
then reconsider b = x as Element of A ;
A14: b in fC2 by A13, Th24;
A15: b < a1 by A13, Th24;
then  b < a2 by A7, Th5;
then  b in InitSegm (fC2,a2) by A14, Th24;
then  b in fC1 by A8, Th24;
hence  x in InitSegm (fC1,a1) by A15, Th24; ::_thesis: verum
end;
 a1 in InitSegm (fC2,a2) by A6, A7, A8, Th24;
then  a1 in fC2 by XBOOLE_0:def_4;
then  a1 in fC1 /\ fC2 by A6, XBOOLE_0:def_4;
hence  a1 in N by A9; ::_thesis: verum
end;
A16: now__::_thesis:_for_a1,_a2_being_Element_of_A_st_a2_in_N_&_a1_in_fC2_&_a1_<_a2_holds_
a1_in_N
let a1, a2 be Element of A; ::_thesis: ( a2 in N & a1 in fC2 & a1 < a2 implies a1 in N )
assume that
A17: a2 in N and
A18: a1 in fC2 and
A19: a1 < a2 ; ::_thesis: a1 in N
A20: ex a being Element of A st
( a = a2 & a in fC1 /\ fC2 & InitSegm (fC1,a) = InitSegm (fC2,a) ) by A17;
A21: InitSegm (fC1,a1) = InitSegm (fC2,a1)
proof
thus  InitSegm (fC1,a1) c= InitSegm (fC2,a1) :: according to XBOOLE_0:def_10 ::_thesis: InitSegm (fC2,a1) c= InitSegm (fC1,a1)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in InitSegm (fC1,a1) or x in InitSegm (fC2,a1) )
assume A22: x in InitSegm (fC1,a1) ; ::_thesis: x in InitSegm (fC2,a1)
then reconsider b = x as Element of A ;
A23: b in fC1 by A22, Th24;
A24: b < a1 by A22, Th24;
then  b < a2 by A19, Th5;
then  b in InitSegm (fC1,a2) by A23, Th24;
then  b in fC2 by A20, Th24;
hence  x in InitSegm (fC2,a1) by A24, Th24; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in InitSegm (fC2,a1) or x in InitSegm (fC1,a1) )
assume A25: x in InitSegm (fC2,a1) ; ::_thesis: x in InitSegm (fC1,a1)
then reconsider b = x as Element of A ;
A26: b in fC2 by A25, Th24;
A27: b < a1 by A25, Th24;
then  b < a2 by A19, Th5;
then  b in InitSegm (fC2,a2) by A26, Th24;
then  b in fC1 by A20, Th24;
hence  x in InitSegm (fC1,a1) by A27, Th24; ::_thesis: verum
end;
 a1 in InitSegm (fC1,a2) by A18, A19, A20, Th24;
then  a1 in fC1 by XBOOLE_0:def_4;
then  a1 in fC1 /\ fC2 by A18, XBOOLE_0:def_4;
hence  a1 in N by A21; ::_thesis: verum
end;
A28: ( the InternalRel of A well_orders fC1 & the InternalRel of A well_orders fC2 ) by Def12;
now__::_thesis:_(_fC1_is_Initial_Segm_of_fC2_iff_fC2_is_not_Initial_Segm_of_fC1_)
percases ( ( N is Initial_Segm of fC1 & N = fC2 ) or ( N is Initial_Segm of fC2 & N = fC1 ) or ( N = fC1 & N = fC2 ) or ( N is Initial_Segm of fC1 & N is Initial_Segm of fC2 ) ) by A2, A4, A28, A3, A16, Th35;
supposeA29: ( N is Initial_Segm of fC1 & N = fC2 ) ; ::_thesis: ( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 )
 fC1 <> {} by Def12;
hence  ( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 ) by A29, Th31; ::_thesis: verum
end;
supposeA30: ( N is Initial_Segm of fC2 & N = fC1 ) ; ::_thesis: ( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 )
 fC2 <> {} by Def12;
hence  ( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 ) by A30, Th31; ::_thesis: verum
end;
suppose ( N = fC1 & N = fC2 ) ; ::_thesis: ( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 )
hence  ( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 ) by A1; ::_thesis: verum
end;
supposeA31: ( N is Initial_Segm of fC1 & N is Initial_Segm of fC2 ) ; ::_thesis: ( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 )
 fC2 <> {} by Def12;
then consider b being Element of A such that
A32: b in fC2 and
A33: N = InitSegm (fC2,b) by A31, Def11;
 fC1 <> {} by Def12;
then consider a being Element of A such that
A34: a in fC1 and
A35: N = InitSegm (fC1,a) by A31, Def11;
A36: a = f . (UpperCone (InitSegm (fC2,b))) by A34, A35, A33, Def12
.= b by A32, Def12 ;
then  a in fC1 /\ fC2 by A34, A32, XBOOLE_0:def_4;
then  a in N by A35, A33, A36;
hence  ( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 ) by A35, Th26; ::_thesis: verum
end;
end;
end;
hence  ( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 ) ; ::_thesis: verum
end;

theorem Th42: :: ORDERS_2:42
for A being non empty Poset
for f being Choice_Function of BOOL the carrier of A
for fC1, fC2 being Chain of f holds
( fC1 c< fC2 iff fC1 is Initial_Segm of fC2 )
proof
let A be non empty Poset; ::_thesis: for f being Choice_Function of BOOL the carrier of A
for fC1, fC2 being Chain of f holds
( fC1 c< fC2 iff fC1 is Initial_Segm of fC2 )
let f be Choice_Function of BOOL the carrier of A; ::_thesis: for fC1, fC2 being Chain of f holds
( fC1 c< fC2 iff fC1 is Initial_Segm of fC2 )
let fC1, fC2 be Chain of f; ::_thesis: ( fC1 c< fC2 iff fC1 is Initial_Segm of fC2 )
thus  ( fC1 c< fC2 implies fC1 is Initial_Segm of fC2 ) ::_thesis: ( fC1 is Initial_Segm of fC2 implies fC1 c< fC2 )
proof
assume A1: fC1 c< fC2 ; ::_thesis: fC1 is Initial_Segm of fC2
now__::_thesis:_fC2_is_not_Initial_Segm_of_fC1
assume A2: fC2 is Initial_Segm of fC1 ; ::_thesis: contradiction
 fC1 <> {} by Def12;
then  ex a being Element of A st
( a in fC1 & fC2 = InitSegm (fC1,a) ) by A2, Def11;
then  fC2 c= fC1 by XBOOLE_1:17;
hence  contradiction by A1, XBOOLE_0:def_8; ::_thesis: verum
end;
hence  fC1 is Initial_Segm of fC2 by A1, Th41; ::_thesis: verum
end;
assume A3: fC1 is Initial_Segm of fC2 ; ::_thesis: fC1 c< fC2
A4: fC2 <> {} by Def12;
then  ex a being Element of A st
( a in fC2 & fC1 = InitSegm (fC2,a) ) by A3, Def11;
then A5: fC1 c= fC2 by XBOOLE_1:17;
 fC1 <> fC2 by A3, A4, Th30;
hence  fC1 c< fC2 by A5, XBOOLE_0:def_8; ::_thesis: verum
end;

definition
let A be non empty Poset;
let f be Choice_Function of BOOL the carrier of A;
func Chains f ->  set  means :Def13: :: ORDERS_2:def 13
 for x being set holds
( x in it iff x is Chain of f );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff x is Chain of f )
proof
defpred S1[ set ] means $1 is Chain of f;
consider X being set  such that
A1: for x being set holds
( x in X iff ( x in bool the carrier of A & S1[x] ) ) from XBOOLE_0:sch_1();
take  X ; ::_thesis: for x being set holds
( x in X iff x is Chain of f )
let x be set ; ::_thesis: ( x in X iff x is Chain of f )
thus  ( x in X implies x is Chain of f ) by A1; ::_thesis: ( x is Chain of f implies x in X )
assume  x is Chain of f ; ::_thesis: x in X
hence  x in X by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff x is Chain of f ) ) & ( for x being set holds
( x in b2 iff x is Chain of f ) ) holds
b1 = b2
proof
let D1, D2 be set ; ::_thesis: ( ( for x being set holds
( x in D1 iff x is Chain of f ) ) & ( for x being set holds
( x in D2 iff x is Chain of f ) ) implies D1 = D2 )
assume A2: for x being set holds
( x in D1 iff x is Chain of f ) ; ::_thesis: ( ex x being set st
( ( x in D2 implies x is Chain of f ) implies ( x is Chain of f & not x in D2 ) ) or D1 = D2 )
assume A3: for x being set holds
( x in D2 iff x is Chain of f ) ; ::_thesis: D1 = D2
thus  D1 c= D2 :: according to XBOOLE_0:def_10 ::_thesis: D2 c= D1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D1 or x in D2 )
assume  x in D1 ; ::_thesis: x in D2
then  x is Chain of f by A2;
hence  x in D2 by A3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D2 or x in D1 )
assume  x in D2 ; ::_thesis: x in D1
then  x is Chain of f by A3;
hence  x in D1 by A2; ::_thesis: verum
end;
end;

:: deftheorem Def13 defines Chains ORDERS_2:def_13_:_
 for A being non empty Poset
for f being Choice_Function of BOOL the carrier of A
for b3 being set holds
( b3 = Chains f iff for x being set holds
( x in b3 iff x is Chain of f ) );

registration
let A be non empty Poset;
let f be Choice_Function of BOOL the carrier of A;
cluster Chains f ->  non empty ;
coherence
 not Chains f is empty
proof
set x = the Chain of f;
 the Chain of f in Chains f by Def13;
hence  not Chains f is empty ; ::_thesis: verum
end;
end;

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 A
proof
let A be non empty Poset; ::_thesis: for f being Choice_Function of BOOL the carrier of A holds union (Chains f) is Subset of A
let f be Choice_Function of BOOL the carrier of A; ::_thesis: union (Chains f) is Subset of A
now__::_thesis:_for_X_being_set_st_X_in_Chains_f_holds_
X_c=_the_carrier_of_A
let X be set ; ::_thesis: ( X in Chains f implies X c= the carrier of A )
assume  X in Chains f ; ::_thesis: X c= the carrier of A
then  X is Chain of f by Def13;
hence  X c= the carrier of A ; ::_thesis: verum
end;
hence  union (Chains f) is Subset of A by ZFMISC_1:76; ::_thesis: verum
end;

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
proof
let A be non empty Poset; ::_thesis: for f being Choice_Function of BOOL the carrier of A holds union (Chains f) is Chain of A
let f be Choice_Function of BOOL the carrier of A; ::_thesis: union (Chains f) is Chain of A
reconsider C = union (Chains f) as Subset of A by Lm2;
 the InternalRel of A is_strongly_connected_in C
proof
let x be set ; :: according to RELAT_2:def_7 ::_thesis: for b1 being set holds
( not x in C or not b1 in C or [x,b1] in the InternalRel of A or [b1,x] in the InternalRel of A )
let y be set ; ::_thesis: ( not x in C or not y in C or [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
assume that
A1: x in C and
A2: y in C ; ::_thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
consider X being set  such that
A3: x in X and
A4: X in Chains f by A1, TARSKI:def_4;
consider Y being set  such that
A5: y in Y and
A6: Y in Chains f by A2, TARSKI:def_4;
reconsider X = X, Y = Y as Chain of f by A4, A6, Def13;
A7: the InternalRel of A is_strongly_connected_in X by Def7;
A8: the InternalRel of A is_strongly_connected_in Y by Def7;
now__::_thesis:_(_[x,y]_in_the_InternalRel_of_A_or_[y,x]_in_the_InternalRel_of_A_)
percases ( X = Y or X <> Y ) ;
suppose X = Y ; ::_thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
hence  ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by A3, A5, A7, RELAT_2:def_7; ::_thesis: verum
end;
supposeA9: X <> Y ; ::_thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
now__::_thesis:_(_[x,y]_in_the_InternalRel_of_A_or_[y,x]_in_the_InternalRel_of_A_)
percases ( X is Initial_Segm of Y or Y is Initial_Segm of X ) by A9, Th41;
suppose X is Initial_Segm of Y ; ::_thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
then  X c< Y by Th42;
then  X c= Y by XBOOLE_0:def_8;
hence  ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by A3, A5, A8, RELAT_2:def_7; ::_thesis: verum
end;
suppose Y is Initial_Segm of X ; ::_thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
then  Y c< X by Th42;
then  Y c= X by XBOOLE_0:def_8;
hence  ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by A3, A5, A7, RELAT_2:def_7; ::_thesis: verum
end;
end;
end;
hence  ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) ; ::_thesis: verum
end;
end;
end;
hence  ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) ; ::_thesis: verum
end;
hence  union (Chains f) is Chain of A by Def7; ::_thesis: verum
end;

theorem Th43: :: ORDERS_2:43
for A being non empty Poset
for f being Choice_Function of BOOL the carrier of A holds union (Chains f) <> {}
proof
let A be non empty Poset; ::_thesis: for f being Choice_Function of BOOL the carrier of A holds union (Chains f) <> {}
let f be Choice_Function of BOOL the carrier of A; ::_thesis: union (Chains f) <> {}
 {(f . the carrier of A)} is Chain of f by Th36;
then  {(f . the carrier of A)} in Chains f by Def13;
hence  union (Chains f) <> {} by ORDERS_1:6; ::_thesis: verum
end;

theorem Th44: :: ORDERS_2:44
for A being non empty Poset
for S being Subset of A
for f being Choice_Function of BOOL the carrier of A
for fC being Chain of f st fC <> union (Chains f) & S = union (Chains f) holds
fC is Initial_Segm of S
proof
let A be non empty Poset; ::_thesis: for S being Subset of A
for f being Choice_Function of BOOL the carrier of A
for fC being Chain of f st fC <> union (Chains f) & S = union (Chains f) holds
fC is Initial_Segm of S
let S be Subset of A; ::_thesis: for f being Choice_Function of BOOL the carrier of A
for fC being Chain of f st fC <> union (Chains f) & S = union (Chains f) holds
fC is Initial_Segm of S
let f be Choice_Function of BOOL the carrier of A; ::_thesis: for fC being Chain of f st fC <> union (Chains f) & S = union (Chains f) holds
fC is Initial_Segm of S
let fC be Chain of f; ::_thesis: ( fC <> union (Chains f) & S = union (Chains f) implies fC is Initial_Segm of S )
assume that
A1: fC <> union (Chains f) and
A2: S = union (Chains f) ; ::_thesis: fC is Initial_Segm of S
set x = the Element of S \ fC;
 fC in Chains f by Def13;
then  fC c= union (Chains f) by ZFMISC_1:74;
then  not union (Chains f) c= fC by A1, XBOOLE_0:def_10;
then A3: S \ fC <> {} by A2, XBOOLE_1:37;
then A4: not the Element of S \ fC in fC by XBOOLE_0:def_5;
 the Element of S \ fC in S by A3, XBOOLE_0:def_5;
then consider X being set  such that
A5: the Element of S \ fC in X and
A6: X in Chains f by A2, TARSKI:def_4;
reconsider X = X as Chain of f by A6, Def13;
 not X c= fC by A3, A5, XBOOLE_0:def_5;
then  not X c< fC by XBOOLE_0:def_8;
then  X is not Initial_Segm of fC by Th42;
then  fC is Initial_Segm of X by A5, A4, Th41;
then consider a being Element of A such that
A7: a in X and
A8: fC = InitSegm (X,a) by A5, Def11;
A9: X c= S by A2, A6, ZFMISC_1:74;
 InitSegm (S,a) = InitSegm (X,a)
proof
thus  InitSegm (S,a) c= InitSegm (X,a) :: according to XBOOLE_0:def_10 ::_thesis: InitSegm (X,a) c= InitSegm (S,a)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in InitSegm (S,a) or x in InitSegm (X,a) )
assume A10: x in InitSegm (S,a) ; ::_thesis: x in InitSegm (X,a)
then A11: x in LowerCone {a} by XBOOLE_0:def_4;
then consider b being Element of A such that
A12: b = x and
A13: for a2 being Element of A st a2 in {a} holds
b < a2 ;
 b in S by A10, A12, XBOOLE_0:def_4;
then consider Y being set  such that
A14: b in Y and
A15: Y in Chains f by A2, TARSKI:def_4;
reconsider Y = Y as Chain of f by A15, Def13;
 a in {a} by TARSKI:def_1;
then A16: b < a by A13;
now__::_thesis:_x_in_InitSegm_(X,a)
percases ( X = Y or X <> Y ) ;
suppose X = Y ; ::_thesis: x in InitSegm (X,a)
hence  x in InitSegm (X,a) by A11, A12, A14, XBOOLE_0:def_4; ::_thesis: verum
end;
supposeA17: X <> Y ; ::_thesis: x in InitSegm (X,a)
now__::_thesis:_x_in_InitSegm_(X,a)
percases ( X is Initial_Segm of Y or Y is Initial_Segm of X ) by A17, Th41;
suppose X is Initial_Segm of Y ; ::_thesis: x in InitSegm (X,a)
then  x in X by A7, A12, A16, A14, Th32;
hence  x in InitSegm (X,a) by A11, XBOOLE_0:def_4; ::_thesis: verum
end;
suppose Y is Initial_Segm of X ; ::_thesis: x in InitSegm (X,a)
then  Y c< X by Th42;
then  Y c= X by XBOOLE_0:def_8;
hence  x in InitSegm (X,a) by A11, A12, A14, XBOOLE_0:def_4; ::_thesis: verum
end;
end;
end;
hence  x in InitSegm (X,a) ; ::_thesis: verum
end;
end;
end;
hence  x in InitSegm (X,a) ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in InitSegm (X,a) or x in InitSegm (S,a) )
assume  x in InitSegm (X,a) ; ::_thesis: x in InitSegm (S,a)
then  ( x in LowerCone {a} & x in X ) by XBOOLE_0:def_4;
hence  x in InitSegm (S,a) by A9, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  fC is Initial_Segm of S by A7, A8, A9, Def11; ::_thesis: verum
end;

theorem Th45: :: ORDERS_2:45
for A being non empty Poset
for f being Choice_Function of BOOL the carrier of A holds union (Chains f) is Chain of f
proof
let A be non empty Poset; ::_thesis: for f being Choice_Function of BOOL the carrier of A holds union (Chains f) is Chain of f
let f be Choice_Function of BOOL the carrier of A; ::_thesis: union (Chains f) is Chain of f
reconsider C = union (Chains f) as Chain of A by Lm3;
A1: now__::_thesis:_for_a_being_Element_of_A_st_a_in_C_holds_
f_._(UpperCone_(InitSegm_(C,a)))_=_a
let a be Element of A; ::_thesis: ( a in C implies f . (UpperCone (InitSegm (C,a))) = a )
assume  a in C ; ::_thesis: f . (UpperCone (InitSegm (C,a))) = a
then consider X being set  such that
A2: a in X and
A3: X in Chains f by TARSKI:def_4;
reconsider X = X as Chain of f by A3, Def13;
now__::_thesis:_f_._(UpperCone_(InitSegm_(C,a)))_=_a
 InitSegm (C,a) = InitSegm (X,a) by A2, Th33, Th44;
hence  f . (UpperCone (InitSegm (C,a))) = a by A2, Def12; ::_thesis: verum
end;
hence  f . (UpperCone (InitSegm (C,a))) = a ; ::_thesis: verum
end;
A4: the InternalRel of A well_orders C
proof
A5: the InternalRel of A is_antisymmetric_in the carrier of A by Def4;
 ( the InternalRel of A is_reflexive_in the carrier of A & the InternalRel of A is_transitive_in the carrier of A ) by Def2, Def3;
hence  ( the InternalRel of A is_reflexive_in C & the InternalRel of A is_transitive_in C & the InternalRel of A is_antisymmetric_in C ) by A5, ORDERS_1:8, ORDERS_1:9, ORDERS_1:10; :: according to WELLORD1:def_5 ::_thesis: ( the InternalRel of A is_connected_in C & the InternalRel of A is_well_founded_in C )
 the InternalRel of A is_strongly_connected_in C by Def7;
hence  the InternalRel of A is_connected_in C by ORDERS_1:7; ::_thesis: the InternalRel of A is_well_founded_in C
let Y be set ; :: according to WELLORD1:def_3 ::_thesis: ( not Y c= C or Y = {} or ex b1 being set st
( b1 in Y & the InternalRel of A -Seg b1 misses Y ) )
set x = the Element of Y;
assume that
A6: Y c= C and
A7: Y <> {} ; ::_thesis: ex b1 being set st
( b1 in Y & the InternalRel of A -Seg b1 misses Y )
 the Element of Y in C by A6, A7, TARSKI:def_3;
then consider X being set  such that
A8: the Element of Y in X and
A9: X in Chains f by TARSKI:def_4;
reconsider X = X as Chain of f by A9, Def13;
A10: the InternalRel of A well_orders X by Def12;
 X /\ Y <> {} by A7, A8, XBOOLE_0:def_4;
then consider a being set  such that
A11: a in X /\ Y and
A12: for x being set st x in X /\ Y holds
[a,x] in the InternalRel of A by A10, WELLORD1:5, XBOOLE_1:17;
take  a ; ::_thesis: ( a in Y & the InternalRel of A -Seg a misses Y )
thus  a in Y by A11, XBOOLE_0:def_4; ::_thesis: the InternalRel of A -Seg a misses Y
reconsider aa = a as Element of A by A11;
thus  ( the InternalRel of A -Seg a) /\ Y c= {} :: according to XBOOLE_0:def_7,XBOOLE_0:def_10 ::_thesis: {} c= ( the InternalRel of A -Seg a) /\ Y
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in ( the InternalRel of A -Seg a) /\ Y or y in {} )
assume A13: y in ( the InternalRel of A -Seg a) /\ Y ; ::_thesis: y in {}
then A14: y in Y by XBOOLE_0:def_4;
then  y in C by A6;
then reconsider b = y as Element of A ;
A15: y in the InternalRel of A -Seg a by A13, XBOOLE_0:def_4;
then A16: y <> a by WELLORD1:1;
 [y,a] in the InternalRel of A by A15, WELLORD1:1;
then A17: b <= aa by Def5;
now__::_thesis:_y_in_X
percases ( X <> C or X = C ) ;
supposeA18: X <> C ; ::_thesis: y in X
 ( a in X & b < aa ) by A11, A16, A17, Def6, XBOOLE_0:def_4;
hence  y in X by A6, A14, A18, Th32, Th44; ::_thesis: verum
end;
suppose X = C ; ::_thesis: y in X
hence  y in X by A6, A14; ::_thesis: verum
end;
end;
end;
then  y in X /\ Y by A14, XBOOLE_0:def_4;
then  [a,y] in the InternalRel of A by A12;
then  aa <= b by Def5;
hence  y in {} by A16, A17, Th2; ::_thesis: verum
end;
thus  {} c= ( the InternalRel of A -Seg a) /\ Y by XBOOLE_1:2; ::_thesis: verum
end;
 C <> {} by Th43;
hence  union (Chains f) is Chain of f by A4, A1, Def12; ::_thesis: verum
end;

begin


theorem Th46: :: ORDERS_2:46
for A being non empty Poset
for S being Subset of A holds field ( the InternalRel of A |_2 S) = S
proof
let A be non empty Poset; ::_thesis: for S being Subset of A holds field ( the InternalRel of A |_2 S) = S
let S be Subset of A; ::_thesis: field ( the InternalRel of A |_2 S) = S
set P = the InternalRel of A |_2 S;
thus  field ( the InternalRel of A |_2 S) c= S by WELLORD1:13; :: according to XBOOLE_0:def_10 ::_thesis: S c= field ( the InternalRel of A |_2 S)
thus  S c= field ( the InternalRel of A |_2 S) ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in S or x in field ( the InternalRel of A |_2 S) )
assume A1: x in S ; ::_thesis: x in field ( the InternalRel of A |_2 S)
then A2: [x,x] in [:S,S:] by ZFMISC_1:87;
 the InternalRel of A is_reflexive_in the carrier of A by Def2;
then  [x,x] in the InternalRel of A by A1, RELAT_2:def_1;
then  [x,x] in the InternalRel of A |_2 S by A2, XBOOLE_0:def_4;
then  x in dom ( the InternalRel of A |_2 S) by XTUPLE_0:def_12;
hence  x in field ( the InternalRel of A |_2 S) by XBOOLE_0:def_3; ::_thesis: verum
end;
end;

theorem :: ORDERS_2:47
for A being non empty Poset
for S being Subset of A st the InternalRel of A |_2 S is being_linear-order holds
S is Chain of A
proof
let A be non empty Poset; ::_thesis: for S being Subset of A st the InternalRel of A |_2 S is being_linear-order holds
S is Chain of A
let S be Subset of A; ::_thesis: ( the InternalRel of A |_2 S is being_linear-order implies S is Chain of A )
assume  the InternalRel of A |_2 S is being_linear-order ; ::_thesis: S is Chain of A
then A1: the InternalRel of A |_2 S is connected by ORDERS_1:def_5;
 field ( the InternalRel of A |_2 S) = S by Th46;
then A2: the InternalRel of A |_2 S is_connected_in S by A1, RELAT_2:def_14;
 S is strongly_connected
proof
let x be set ; :: according to RELAT_2:def_7,ORDERS_2:def_7 ::_thesis: for b1 being set holds
( not x in S or not b1 in S or [x,b1] in the InternalRel of A or [b1,x] in the InternalRel of A )
let y be set ; ::_thesis: ( not x in S or not y in S or [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
assume A3: ( x in S & y in S ) ; ::_thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
then reconsider a = x, b = y as Element of A ;
now__::_thesis:_(_[x,y]_in_the_InternalRel_of_A_or_[y,x]_in_the_InternalRel_of_A_)
percases ( x = y or x <> y ) ;
suppose x = y ; ::_thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
then  a <= b ;
hence  ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by Def5; ::_thesis: verum
end;
suppose x <> y ; ::_thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
then  ( [x,y] in the InternalRel of A |_2 S or [y,x] in the InternalRel of A |_2 S ) by A2, A3, RELAT_2:def_6;
hence  ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by XBOOLE_0:def_4; ::_thesis: verum
end;
end;
end;
hence  ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) ; ::_thesis: verum
end;
hence  S is Chain of A ; ::_thesis: verum
end;

theorem :: ORDERS_2:48
for A being non empty Poset
for C being Chain of A holds the InternalRel of A |_2 C is being_linear-order
proof
let A be non empty Poset; ::_thesis: for C being Chain of A holds the InternalRel of A |_2 C is being_linear-order
let C be Chain of A; ::_thesis: the InternalRel of A |_2 C is being_linear-order
set P = the InternalRel of A |_2 C;
A1: the InternalRel of A |_2 C is_connected_in C
proof
let x be set ; :: according to RELAT_2:def_6 ::_thesis: for b1 being set holds
( not x in C or not b1 in C or x = b1 or [x,b1] in the InternalRel of A |_2 C or [b1,x] in the InternalRel of A |_2 C )
let y be set ; ::_thesis: ( not x in C or not y in C or x = y or [x,y] in the InternalRel of A |_2 C or [y,x] in the InternalRel of A |_2 C )
assume A2: ( x in C & y in C ) ; ::_thesis: ( x = y or [x,y] in the InternalRel of A |_2 C or [y,x] in the InternalRel of A |_2 C )
then A3: ( [x,y] in [:C,C:] & [y,x] in [:C,C:] ) by ZFMISC_1:87;
 the InternalRel of A is_strongly_connected_in C by Def7;
then  ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by A2, RELAT_2:def_7;
hence  ( x = y or [x,y] in the InternalRel of A |_2 C or [y,x] in the InternalRel of A |_2 C ) by A3, XBOOLE_0:def_4; ::_thesis: verum
end;
 the InternalRel of A is being_partial-order by ORDERS_1:def_4;
then  the InternalRel of A |_2 C is being_partial-order by ORDERS_1:26;
hence  ( the InternalRel of A |_2 C is reflexive & the InternalRel of A |_2 C is transitive & the InternalRel of A |_2 C is antisymmetric ) by ORDERS_1:def_4; :: according to ORDERS_1:def_5 ::_thesis: the InternalRel of A |_2 C is connected
 C = field ( the InternalRel of A |_2 C) by Th46;
hence  the InternalRel of A |_2 C is connected by A1, RELAT_2:def_14; ::_thesis: verum
end;

theorem :: ORDERS_2:49
for A being non empty Poset
for S being Subset of A st the InternalRel of A linearly_orders S holds
S is Chain of A
proof
let A be non empty Poset; ::_thesis: for S being Subset of A st the InternalRel of A linearly_orders S holds
S is Chain of A
let S be Subset of A; ::_thesis: ( the InternalRel of A linearly_orders S implies S is Chain of A )
assume  the InternalRel of A linearly_orders S ; ::_thesis: S is Chain of A
then  ( the InternalRel of A is_reflexive_in S & the InternalRel of A is_connected_in S ) by ORDERS_1:def_8;
then  the InternalRel of A is_strongly_connected_in S by ORDERS_1:7;
hence  S is Chain of A by Def7; ::_thesis: verum
end;

theorem :: ORDERS_2:50
for A being non empty Poset
for C being Chain of A holds the InternalRel of A linearly_orders C
proof
let A be non empty Poset; ::_thesis: for C being Chain of A holds the InternalRel of A linearly_orders C
let C be Chain of A; ::_thesis: the InternalRel of A linearly_orders C
A1: the InternalRel of A is_antisymmetric_in the carrier of A by Def4;
 ( the InternalRel of A is_reflexive_in the carrier of A & the InternalRel of A is_transitive_in the carrier of A ) by Def2, Def3;
hence  ( the InternalRel of A is_reflexive_in C & the InternalRel of A is_transitive_in C & the InternalRel of A is_antisymmetric_in C ) by A1, ORDERS_1:8, ORDERS_1:9, ORDERS_1:10; :: according to ORDERS_1:def_8 ::_thesis: the InternalRel of A is_connected_in C
 the InternalRel of A is_strongly_connected_in C by Def7;
hence  the InternalRel of A is_connected_in C by ORDERS_1:7; ::_thesis: verum
end;

theorem :: ORDERS_2:51
for A being non empty Poset
for a being Element of A holds
( a is_minimal_in the InternalRel of A iff for b being Element of A holds not b < a )
proof
let A be non empty Poset; ::_thesis: for a being Element of A holds
( a is_minimal_in the InternalRel of A iff for b being Element of A holds not b < a )
let a be Element of A; ::_thesis: ( a is_minimal_in the InternalRel of A iff for b being Element of A holds not b < a )
A1: the carrier of A = field the InternalRel of A by ORDERS_1:15;
thus  ( a is_minimal_in the InternalRel of A implies for b being Element of A holds not b < a ) ::_thesis: ( ( for b being Element of A holds not b < a ) implies a is_minimal_in the InternalRel of A )
proof
assume A2: a is_minimal_in the InternalRel of A ; ::_thesis: for b being Element of A holds not b < a
let b be Element of A; ::_thesis: not b < a
 ( a = b or not [b,a] in the InternalRel of A ) by A1, A2, ORDERS_1:def_12;
then  ( a = b or not b <= a ) by Def5;
hence  not b < a by Def6; ::_thesis: verum
end;
assume A3: for b being Element of A holds not b < a ; ::_thesis: a is_minimal_in the InternalRel of A
thus  a in field the InternalRel of A by A1; :: according to ORDERS_1:def_12 ::_thesis: for b1 being set holds
( not b1 in field the InternalRel of A or b1 = a or not [b1,a] in the InternalRel of A )
let y be set ; ::_thesis: ( not y in field the InternalRel of A or y = a or not [y,a] in the InternalRel of A )
assume that
A4: y in field the InternalRel of A and
A5: y <> a and
A6: [y,a] in the InternalRel of A ; ::_thesis: contradiction
reconsider b = y as Element of A by A4, ORDERS_1:15;
 b <= a by A6, Def5;
then  b < a by A5, Def6;
hence  contradiction by A3; ::_thesis: verum
end;

theorem :: ORDERS_2:52
for A being non empty Poset
for a being Element of A holds
( a is_maximal_in the InternalRel of A iff for b being Element of A holds not a < b )
proof
let A be non empty Poset; ::_thesis: for a being Element of A holds
( a is_maximal_in the InternalRel of A iff for b being Element of A holds not a < b )
let a be Element of A; ::_thesis: ( a is_maximal_in the InternalRel of A iff for b being Element of A holds not a < b )
A1: the carrier of A = field the InternalRel of A by ORDERS_1:15;
thus  ( a is_maximal_in the InternalRel of A implies for b being Element of A holds not a < b ) ::_thesis: ( ( for b being Element of A holds not a < b ) implies a is_maximal_in the InternalRel of A )
proof
assume A2: a is_maximal_in the InternalRel of A ; ::_thesis: for b being Element of A holds not a < b
let b be Element of A; ::_thesis: not a < b
 ( a = b or not [a,b] in the InternalRel of A ) by A1, A2, ORDERS_1:def_11;
then  ( a = b or not a <= b ) by Def5;
hence  not a < b by Def6; ::_thesis: verum
end;
assume A3: for b being Element of A holds not a < b ; ::_thesis: a is_maximal_in the InternalRel of A
thus  a in field the InternalRel of A by A1; :: according to ORDERS_1:def_11 ::_thesis: for b1 being set holds
( not b1 in field the InternalRel of A or b1 = a or not [a,b1] in the InternalRel of A )
let y be set ; ::_thesis: ( not y in field the InternalRel of A or y = a or not [a,y] in the InternalRel of A )
assume that
A4: y in field the InternalRel of A and
A5: y <> a and
A6: [a,y] in the InternalRel of A ; ::_thesis: contradiction
reconsider b = y as Element of A by A4, ORDERS_1:15;
 a <= b by A6, Def5;
then  a < b by A5, Def6;
hence  contradiction by A3; ::_thesis: verum
end;

theorem :: ORDERS_2:53
for A being non empty Poset
for a being Element of A holds
( a is_superior_of the InternalRel of A iff for b being Element of A st a <> b holds
b < a )
proof
let A be non empty Poset; ::_thesis: for a being Element of A holds
( a is_superior_of the InternalRel of A iff for b being Element of A st a <> b holds
b < a )
let a be Element of A; ::_thesis: ( a is_superior_of the InternalRel of A iff for b being Element of A st a <> b holds
b < a )
A1: the carrier of A = field the InternalRel of A by ORDERS_1:15;
thus  ( a is_superior_of the InternalRel of A implies for b being Element of A st a <> b holds
b < a ) ::_thesis: ( ( for b being Element of A st a <> b holds
b < a ) implies a is_superior_of the InternalRel of A )
proof
assume A2: a is_superior_of the InternalRel of A ; ::_thesis: for b being Element of A st a <> b holds
b < a
let b be Element of A; ::_thesis: ( a <> b implies b < a )
assume A3: a <> b ; ::_thesis: b < a
then  [b,a] in the InternalRel of A by A1, A2, ORDERS_1:def_13;
then  b <= a by Def5;
hence  b < a by A3, Def6; ::_thesis: verum
end;
assume A4: for b being Element of A st a <> b holds
b < a ; ::_thesis: a is_superior_of the InternalRel of A
thus  a in field the InternalRel of A by A1; :: according to ORDERS_1:def_13 ::_thesis: for b1 being set holds
( not b1 in field the InternalRel of A or b1 = a or [b1,a] in the InternalRel of A )
let y be set ; ::_thesis: ( not y in field the InternalRel of A or y = a or [y,a] in the InternalRel of A )
assume  y in field the InternalRel of A ; ::_thesis: ( y = a or [y,a] in the InternalRel of A )
then reconsider b = y as Element of A by ORDERS_1:15;
assume  y <> a ; ::_thesis: [y,a] in the InternalRel of A
then  b < a by A4;
then  b <= a by Def6;
hence  [y,a] in the InternalRel of A by Def5; ::_thesis: verum
end;

theorem :: ORDERS_2:54
for A being non empty Poset
for a being Element of A holds
( a is_inferior_of the InternalRel of A iff for b being Element of A st a <> b holds
a < b )
proof
let A be non empty Poset; ::_thesis: for a being Element of A holds
( a is_inferior_of the InternalRel of A iff for b being Element of A st a <> b holds
a < b )
let a be Element of A; ::_thesis: ( a is_inferior_of the InternalRel of A iff for b being Element of A st a <> b holds
a < b )
A1: the carrier of A = field the InternalRel of A by ORDERS_1:15;
thus  ( a is_inferior_of the InternalRel of A implies for b being Element of A st a <> b holds
a < b ) ::_thesis: ( ( for b being Element of A st a <> b holds
a < b ) implies a is_inferior_of the InternalRel of A )
proof
assume A2: a is_inferior_of the InternalRel of A ; ::_thesis: for b being Element of A st a <> b holds
a < b
let b be Element of A; ::_thesis: ( a <> b implies a < b )
assume A3: a <> b ; ::_thesis: a < b
then  [a,b] in the InternalRel of A by A1, A2, ORDERS_1:def_14;
then  a <= b by Def5;
hence  a < b by A3, Def6; ::_thesis: verum
end;
assume A4: for b being Element of A st a <> b holds
a < b ; ::_thesis: a is_inferior_of the InternalRel of A
thus  a in field the InternalRel of A by A1; :: according to ORDERS_1:def_14 ::_thesis: for b1 being set holds
( not b1 in field the InternalRel of A or b1 = a or [a,b1] in the InternalRel of A )
let y be set ; ::_thesis: ( not y in field the InternalRel of A or y = a or [a,y] in the InternalRel of A )
assume  y in field the InternalRel of A ; ::_thesis: ( y = a or [a,y] in the InternalRel of A )
then reconsider b = y as Element of A by ORDERS_1:15;
assume  y <> a ; ::_thesis: [a,y] in the InternalRel of A
then  a < b by A4;
then  a <= b by Def6;
hence  [a,y] in the InternalRel of A by Def5; ::_thesis: verum
end;

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
proof
let X, Y be set ; ::_thesis: for R being Relation st R is_connected_in X & Y c= X holds
R is_connected_in Y
let R be Relation; ::_thesis: ( R is_connected_in X & Y c= X implies R is_connected_in Y )
assume A1: ( R is_connected_in X & Y c= X ) ; ::_thesis: R is_connected_in Y
let x be set ; :: according to RELAT_2:def_6 ::_thesis: for b1 being set holds
( not x in Y or not b1 in Y or x = b1 or [x,b1] in R or [b1,x] in R )
let y be set ; ::_thesis: ( not x in Y or not y in Y or x = y or [x,y] in R or [y,x] in R )
assume  ( x in Y & y in Y ) ; ::_thesis: ( x = y or [x,y] in R or [y,x] in R )
hence  ( x = y or [x,y] in R or [y,x] in R ) by A1, RELAT_2:def_6; ::_thesis: verum
end;

Lm5:  for X, Y being set
for R being Relation st R well_orders X & Y c= X holds
R well_orders Y
proof
let X, Y be set ; ::_thesis: for R being Relation st R well_orders X & Y c= X holds
R well_orders Y
let R be Relation; ::_thesis: ( R well_orders X & Y c= X implies R well_orders Y )
assume that
A1: R well_orders X and
A2: Y c= X ; ::_thesis: R well_orders Y
A3: ( R is_antisymmetric_in X & R is_connected_in X ) by A1, WELLORD1:def_5;
A4: R is_well_founded_in X by A1, WELLORD1:def_5;
 ( R is_reflexive_in X & R is_transitive_in X ) by A1, WELLORD1:def_5;
hence  ( R is_reflexive_in Y & R is_transitive_in Y & R is_antisymmetric_in Y & R is_connected_in Y ) by A2, A3, Lm4, ORDERS_1:8, ORDERS_1:9, ORDERS_1:10; :: according to WELLORD1:def_5 ::_thesis: R is_well_founded_in Y
let Z be set ; :: according to WELLORD1:def_3 ::_thesis: ( not Z c= Y or Z = {} or ex b1 being set st
( b1 in Z & R -Seg b1 misses Z ) )
assume that
A5: Z c= Y and
A6: Z <> {} ; ::_thesis: ex b1 being set st
( b1 in Z & R -Seg b1 misses Z )
 Z c= X by A2, A5, XBOOLE_1:1;
hence  ex b1 being set st
( b1 in Z & R -Seg b1 misses Z ) by A6, A4, WELLORD1:def_3; ::_thesis: verum
end;

theorem Th55: :: ORDERS_2:55
for A being non empty Poset st ( for C being Chain of A ex a being Element of A st
for b being Element of A st b in C holds
b <= a ) holds
ex a being Element of A st
for b being Element of A holds not a < b
proof
let A be non empty Poset; ::_thesis: ( ( for C being Chain of A ex a being Element of A st
for b being Element of A st b in C holds
b <= a ) implies ex a being Element of A st
for b being Element of A holds not a < b )
set f = the Choice_Function of BOOL the carrier of A;
reconsider F = union (Chains the Choice_Function of BOOL the carrier of A) as Chain of the Choice_Function of BOOL the carrier of A by Th45;
assume  for C being Chain of A ex a being Element of A st
for b being Element of A st b in C holds
b <= a ; ::_thesis: ex a being Element of A st
for b being Element of A holds not a < b
then consider a being Element of A such that
A1: for b being Element of A st b in F holds
b <= a ;
take  a ; ::_thesis: for b being Element of A holds not a < b
let b be Element of A; ::_thesis: not a < b
assume A2: a < b ; ::_thesis: contradiction
now__::_thesis:_for_a1_being_Element_of_A_st_a1_in_F_holds_
a1_<_b
let a1 be Element of A; ::_thesis: ( a1 in F implies a1 < b )
assume  a1 in F ; ::_thesis: a1 < b
then  a1 <= a by A1;
hence  a1 < b by A2, Th7; ::_thesis: verum
end;
then  b in  {  a1 where a1 is Element of A : for a2 being Element of A st a2 in F holds
a2 < a1  }  ;
then  not UpperCone F in {{}} by TARSKI:def_1;
then A3: UpperCone F in BOOL the carrier of A by XBOOLE_0:def_5;
 not {} in BOOL the carrier of A by ORDERS_1:1;
then A4: the Choice_Function of BOOL the carrier of A . (UpperCone F) in UpperCone F by A3, ORDERS_1:def_1;
then reconsider c = the Choice_Function of BOOL the carrier of A . (UpperCone F) as Element of A ;
reconsider Z = F \/ {c} as Subset of A ;
A5: ex c11 being Element of A st
( c11 = c & ( for a2 being Element of A st a2 in F holds
a2 < c11 ) ) by A4;
A6: the InternalRel of A is_connected_in Z
proof
let x be set ; :: according to RELAT_2:def_6 ::_thesis: for b1 being set holds
( not x in Z or not b1 in Z or x = b1 or [x,b1] in the InternalRel of A or [b1,x] in the InternalRel of A )
let y be set ; ::_thesis: ( not x in Z or not y in Z or x = y or [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
assume A7: ( x in Z & y in Z ) ; ::_thesis: ( x = y or [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
then reconsider x1 = x, y1 = y as Element of A ;
now__::_thesis:_(_x_=_y_or_[x,y]_in_the_InternalRel_of_A_or_[y,x]_in_the_InternalRel_of_A_)
percases ( ( x1 in F & y1 in F ) or ( x1 in F & y1 in {c} ) or ( x1 in {c} & y1 in F ) or ( x1 in {c} & y1 in {c} ) ) by A7, XBOOLE_0:def_3;
suppose ( x1 in F & y1 in F ) ; ::_thesis: ( x = y or [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
then  ( x1 <= y1 or y1 <= x1 ) by Th11;
hence  ( x = y or [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by Def5; ::_thesis: verum
end;
supposeA8: ( x1 in F & y1 in {c} ) ; ::_thesis: ( x = y or [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
then  y1 = c by TARSKI:def_1;
then  x1 < y1 by A5, A8;
then  x1 <= y1 by Def6;
hence  ( x = y or [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by Def5; ::_thesis: verum
end;
supposeA9: ( x1 in {c} & y1 in F ) ; ::_thesis: ( x = y or [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
then  x1 = c by TARSKI:def_1;
then  y1 < x1 by A5, A9;
then  y1 <= x1 by Def6;
hence  ( x = y or [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by Def5; ::_thesis: verum
end;
supposeA10: ( x1 in {c} & y1 in {c} ) ; ::_thesis: ( x = y or [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
then  x1 = c by TARSKI:def_1;
hence  ( x = y or [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by A10, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
hence  ( x = y or [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) ; ::_thesis: verum
end;
A11: now__::_thesis:_for_a1_being_Element_of_A_st_a1_in_Z_holds_
the_Choice_Function_of_BOOL_the_carrier_of_A_._(UpperCone_(InitSegm_(Z,a1)))_=_a1
let a1 be Element of A; ::_thesis: ( a1 in Z implies the Choice_Function of BOOL the carrier of A . (UpperCone (InitSegm (Z,a1))) = a1 )
assume A12: a1 in Z ; ::_thesis: the Choice_Function of BOOL the carrier of A . (UpperCone (InitSegm (Z,a1))) = a1
now__::_thesis:_the_Choice_Function_of_BOOL_the_carrier_of_A_._(UpperCone_(InitSegm_(Z,a1)))_=_a1
percases ( a1 = c or a1 <> c ) ;
supposeA13: a1 = c ; ::_thesis: the Choice_Function of BOOL the carrier of A . (UpperCone (InitSegm (Z,a1))) = a1
 InitSegm (Z,c) = F
proof
thus  InitSegm (Z,c) c= F :: according to XBOOLE_0:def_10 ::_thesis: F c= InitSegm (Z,c)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in InitSegm (Z,c) or x in F )
assume that
A14: x in InitSegm (Z,c) and
A15: not x in F ; ::_thesis: contradiction
 x in Z by A14, XBOOLE_0:def_4;
then  x in {c} by A15, XBOOLE_0:def_3;
then A16: x = c by TARSKI:def_1;
 x in LowerCone {c} by A14, XBOOLE_0:def_4;
hence  contradiction by A16, Th21; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F or x in InitSegm (Z,c) )
assume A17: x in F ; ::_thesis: x in InitSegm (Z,c)
then reconsider y = x as Element of A ;
 y < c by A5, A17;
then A18: x in LowerCone {c} by Th23;
 x in Z by A17, XBOOLE_0:def_3;
hence  x in InitSegm (Z,c) by A18, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  the Choice_Function of BOOL the carrier of A . (UpperCone (InitSegm (Z,a1))) = a1 by A13; ::_thesis: verum
end;
suppose a1 <> c ; ::_thesis: the Choice_Function of BOOL the carrier of A . (UpperCone (InitSegm (Z,a1))) = a1
then  not a1 in {c} by TARSKI:def_1;
then A19: a1 in F by A12, XBOOLE_0:def_3;
A20: InitSegm (Z,a1) c= InitSegm (F,a1)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in InitSegm (Z,a1) or x in InitSegm (F,a1) )
assume A21: x in InitSegm (Z,a1) ; ::_thesis: x in InitSegm (F,a1)
then A22: x in LowerCone {a1} by XBOOLE_0:def_4;
now__::_thesis:_x_in_F
assume A23: not x in F ; ::_thesis: contradiction
 x in Z by A21, XBOOLE_0:def_4;
then  x in {c} by A23, XBOOLE_0:def_3;
then  x = c by TARSKI:def_1;
then A24: ex c1 being Element of A st
( c1 = c & ( for c2 being Element of A st c2 in {a1} holds
c1 < c2 ) ) by A22;
A25: a1 < c by A5, A19;
 a1 in {a1} by TARSKI:def_1;
then  c < a1 by A24;
hence  contradiction by A25, Th4; ::_thesis: verum
end;
hence  x in InitSegm (F,a1) by A22, XBOOLE_0:def_4; ::_thesis: verum
end;
 InitSegm (F,a1) c= InitSegm (Z,a1) by Th28, XBOOLE_1:7;
then  InitSegm (Z,a1) = InitSegm (F,a1) by A20, XBOOLE_0:def_10;
hence  the Choice_Function of BOOL the carrier of A . (UpperCone (InitSegm (Z,a1))) = a1 by A19, Def12; ::_thesis: verum
end;
end;
end;
hence  the Choice_Function of BOOL the carrier of A . (UpperCone (InitSegm (Z,a1))) = a1 ; ::_thesis: verum
end;
 the InternalRel of A is_reflexive_in the carrier of A by Def2;
then A26: the InternalRel of A is_reflexive_in Z by ORDERS_1:8;
then  the InternalRel of A is_strongly_connected_in Z by A6, ORDERS_1:7;
then A27: Z is Chain of A by Def7;
A28: the InternalRel of A is_well_founded_in Z
proof
let Y be set ; :: according to WELLORD1:def_3 ::_thesis: ( not Y c= Z or Y = {} or ex b1 being set st
( b1 in Y & the InternalRel of A -Seg b1 misses Y ) )
assume that
A29: Y c= Z and
A30: Y <> {} ; ::_thesis: ex b1 being set st
( b1 in Y & the InternalRel of A -Seg b1 misses Y )
now__::_thesis:_(_(_Y_=_{c}_&_ex_x_being_Element_of_A_st_
(_x_in_Y_&_not_the_InternalRel_of_A_-Seg_x_meets_Y_)_)_or_(_Y_<>_{c}_&_ex_x9_being_set_st_
(_x9_in_Y_&_the_InternalRel_of_A_-Seg_x9_misses_Y_)_)_)
percases ( Y = {c} or Y <> {c} ) ;
caseA31: Y = {c} ; ::_thesis: ex x being Element of A st
( x in Y & not the InternalRel of A -Seg x meets Y )
take x = c; ::_thesis: ( x in Y & not the InternalRel of A -Seg x meets Y )
thus  x in Y by A31, TARSKI:def_1; ::_thesis: not the InternalRel of A -Seg x meets Y
assume  the InternalRel of A -Seg x meets Y ; ::_thesis: contradiction
then consider x9 being set  such that
A32: x9 in the InternalRel of A -Seg x and
A33: x9 in Y by XBOOLE_0:3;
 x9 = c by A31, A33, TARSKI:def_1;
hence  contradiction by A32, WELLORD1:1; ::_thesis: verum
end;
caseA34: Y <> {c} ; ::_thesis: ex x9 being set st
( x9 in Y & the InternalRel of A -Seg x9 misses Y )
set X = Y \ {c};
A35: now__::_thesis:_not_Y_\_{c}_=_{}
assume  Y \ {c} = {} ; ::_thesis: contradiction
then  Y c= {c} by XBOOLE_1:37;
hence  contradiction by A30, A34, ZFMISC_1:33; ::_thesis: verum
end;
A36: Y \ {c} c= F
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Y \ {c} or x in F )
assume that
A37: x in Y \ {c} and
A38: not x in F ; ::_thesis: contradiction
 x in Y by A37;
then  x in {c} by A29, A38, XBOOLE_0:def_3;
hence  contradiction by A37, XBOOLE_0:def_5; ::_thesis: verum
end;
 the InternalRel of A well_orders F by Def12;
then  the InternalRel of A well_orders Y \ {c} by A36, Lm5;
then  the InternalRel of A is_well_founded_in Y \ {c} by WELLORD1:def_5;
then consider x being set  such that
A39: x in Y \ {c} and
A40: the InternalRel of A -Seg x misses Y \ {c} by A35, WELLORD1:def_3;
take x9 = x; ::_thesis: ( x9 in Y & the InternalRel of A -Seg x9 misses Y )
thus  x9 in Y by A39; ::_thesis: the InternalRel of A -Seg x9 misses Y
A41: ( the InternalRel of A -Seg x) /\ (Y \ {c}) = {} by A40, XBOOLE_0:def_7;
now__::_thesis:_the_InternalRel_of_A_-Seg_x9_misses_Y
percases ( c in Y or not c in Y ) ;
supposeA42: c in Y ; ::_thesis: the InternalRel of A -Seg x9 misses Y
A43: now__::_thesis:_not_c_in_the_InternalRel_of_A_-Seg_x9
 x9 in F by A36, A39;
then reconsider x99 = x9 as Element of A ;
assume A44: c in the InternalRel of A -Seg x9 ; ::_thesis: contradiction
then  [c,x9] in the InternalRel of A by WELLORD1:1;
then A45: c <= x99 by Def5;
A46: x99 < c by A5, A36, A39;
 c <> x99 by A44, WELLORD1:1;
then  c < x99 by A45, Def6;
hence  contradiction by A46, Th4; ::_thesis: verum
end;
A47: now__::_thesis:_not_(_the_InternalRel_of_A_-Seg_x9)_/\_{c}_<>_{}
set x = the Element of ( the InternalRel of A -Seg x9) /\ {c};
assume A48: ( the InternalRel of A -Seg x9) /\ {c} <> {} ; ::_thesis: contradiction
then  the Element of ( the InternalRel of A -Seg x9) /\ {c} in {c} by XBOOLE_0:def_4;
then  the Element of ( the InternalRel of A -Seg x9) /\ {c} = c by TARSKI:def_1;
hence  contradiction by A43, A48, XBOOLE_0:def_4; ::_thesis: verum
end;
 {c} c= Y by A42, ZFMISC_1:31;
then  Y = (Y \ {c}) \/ {c} by XBOOLE_1:45;
then ( the InternalRel of A -Seg x9) /\ Y = {} \/ {} by A41, A47, XBOOLE_1:23
.= {} ;
hence  the InternalRel of A -Seg x9 misses Y by XBOOLE_0:def_7; ::_thesis: verum
end;
suppose not c in Y ; ::_thesis: the InternalRel of A -Seg x9 misses Y
then  Y misses {c} by ZFMISC_1:50;
hence  the InternalRel of A -Seg x9 misses Y by A40, XBOOLE_1:83; ::_thesis: verum
end;
end;
end;
hence  the InternalRel of A -Seg x9 misses Y ; ::_thesis: verum
end;
end;
end;
hence  ex b1 being set st
( b1 in Y & the InternalRel of A -Seg b1 misses Y ) ; ::_thesis: verum
end;
 the InternalRel of A is_transitive_in the carrier of A by Def3;
then A49: the InternalRel of A is_transitive_in Z by ORDERS_1:10;
 the InternalRel of A is_antisymmetric_in the carrier of A by Def4;
then  the InternalRel of A is_antisymmetric_in Z by ORDERS_1:9;
then  the InternalRel of A well_orders Z by A26, A49, A6, A28, WELLORD1:def_5;
then reconsider Z = Z as Chain of the Choice_Function of BOOL the carrier of A by A27, A11, Def12;
 c in {c} by TARSKI:def_1;
then A50: c in Z by XBOOLE_0:def_3;
 Z in Chains the Choice_Function of BOOL the carrier of A by Def13;
then  c in F by A50, TARSKI:def_4;
hence  contradiction by A5; ::_thesis: verum
end;

theorem :: ORDERS_2:56
for A being non empty Poset st ( for C being Chain of A ex a being Element of A st
for b being Element of A st b in C holds
a <= b ) holds
ex a being Element of A st
for b being Element of A holds not b < a
proof
let A be non empty Poset; ::_thesis: ( ( for C being Chain of A ex a being Element of A st
for b being Element of A st b in C holds
a <= b ) implies ex a being Element of A st
for b being Element of A holds not b < a )
set X = the carrier of A;
set R = the InternalRel of A ~ ;
A1: dom ( the InternalRel of A ~) = dom the InternalRel of A by RELAT_2:12
.= the carrier of A by PARTFUN1:def_2 ;
A2: for a, b being Element of A holds
( [a,b] in the InternalRel of A ~ iff b <= a )
proof
let a, b be Element of A; ::_thesis: ( [a,b] in the InternalRel of A ~ iff b <= a )
 ( [a,b] in the InternalRel of A ~ iff [b,a] in the InternalRel of A ) by RELAT_1:def_7;
hence  ( [a,b] in the InternalRel of A ~ iff b <= a ) by Def5; ::_thesis: verum
end;
reconsider R = the InternalRel of A ~ as Order of the carrier of A by A1, PARTFUN1:def_2;
set B = RelStr(# the carrier of A,R #);
assume A3: for C being Chain of A ex a being Element of A st
for b being Element of A st b in C holds
a <= b ; ::_thesis: ex a being Element of A st
for b being Element of A holds not b < a
 for E being Chain of RelStr(# the carrier of A,R #) ex e being Element of RelStr(# the carrier of A,R #) st
for f being Element of RelStr(# the carrier of A,R #) st f in E holds
f <= e
proof
let E be Chain of RelStr(# the carrier of A,R #); ::_thesis: ex e being Element of RelStr(# the carrier of A,R #) st
for f being Element of RelStr(# the carrier of A,R #) st f in E holds
f <= e
reconsider C = E as Subset of A ;
 the InternalRel of A is_strongly_connected_in C
proof
let x be set ; :: according to RELAT_2:def_7 ::_thesis: for b1 being set holds
( not x in C or not b1 in C or [x,b1] in the InternalRel of A or [b1,x] in the InternalRel of A )
let y be set ; ::_thesis: ( not x in C or not y in C or [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
assume A4: ( x in C & y in C ) ; ::_thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
then reconsider e = x, f = y as Element of RelStr(# the carrier of A,R #) ;
reconsider e1 = e, f1 = f as Element of A ;
A5: ( e <= f or f <= e ) by A4, Th11;
now__::_thesis:_(_[x,y]_in_the_InternalRel_of_A_or_[y,x]_in_the_InternalRel_of_A_)
percases ( [e,f] in R or [f,e] in R ) by A5, Def5;
suppose [e,f] in R ; ::_thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
then  f1 <= e1 by A2;
hence  ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by Def5; ::_thesis: verum
end;
suppose [f,e] in R ; ::_thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
then  e1 <= f1 by A2;
hence  ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by Def5; ::_thesis: verum
end;
end;
end;
hence  ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) ; ::_thesis: verum
end;
then reconsider C = C as Chain of A by Def7;
consider a being Element of A such that
A6: for b being Element of A st b in C holds
a <= b by A3;
reconsider e = a as Element of RelStr(# the carrier of A,R #) ;
take  e ; ::_thesis: for f being Element of RelStr(# the carrier of A,R #) st f in E holds
f <= e
let f be Element of RelStr(# the carrier of A,R #); ::_thesis: ( f in E implies f <= e )
reconsider b = f as Element of A ;
assume  f in E ; ::_thesis: f <= e
then  a <= b by A6;
then  [f,e] in R by A2;
hence  f <= e by Def5; ::_thesis: verum
end;
then consider e being Element of RelStr(# the carrier of A,R #) such that
A7: for f being Element of RelStr(# the carrier of A,R #) holds not e < f by Th55;
reconsider d = e as Element of A ;
take  d ; ::_thesis: for b being Element of A holds not b < d
let b be Element of A; ::_thesis: not b < d
reconsider f = b as Element of RelStr(# the carrier of A,R #) ;
assume A8: b < d ; ::_thesis: contradiction
then  b <= d by Def6;
then  [e,f] in R by A2;
then  e <= f by Def5;
then  e < f by A8, Def6;
hence  contradiction by A7; ::_thesis: verum
end;

registration
cluster empty strict for RelStr ;
existence
 ex b1 being RelStr st
( b1 is strict & b1 is empty )
proof
take R = RelStr(# {}, the Relation of {} #); ::_thesis: ( R is strict & R is empty )
thus  R is strict ; ::_thesis: R is empty
thus  the carrier of R is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;