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:89;
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, y be object ; :: according to RELAT_2:def 6 :: 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 )

per cases ( ( 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 ) ; :: thesis: verum

end;

suppose A8: ( 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 ;
hence ( x = y or [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) ; :: thesis: verum

end;

suppose A9: ( 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 ;
hence ( x = y or [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) ; :: thesis: verum

end;

suppose A10: ( 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

per cases ( a1 = c or a1 <> c ) ;

suppose A13: 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 object ; :: 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 object ; :: 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 object ; :: 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;
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 ;
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 b₁ being object st
( b₁ in Y & the InternalRel of A -Seg b₁ misses Y ) )
assume that
A29: Y c= Z and
A30: Y <> {} ; :: thesis: ex b₁ being object st
( b₁ in Y & the InternalRel of A -Seg b₁ 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 object st
( x9 in Y & the InternalRel of A -Seg x9 misses Y ) ) )

per cases ( Y = {c} or Y <> {c} ) ;

case A31: 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 object 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;

case A34: Y <> {c} ; :: thesis: ex x9 being object 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 object ; :: 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, Lm4;
then the InternalRel of A is_well_founded_in Y \ {c} ;
then consider x being object such that
A39: x in Y \ {c} and
A40: the InternalRel of A -Seg x misses Y \ {c} by A35;
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;

now :: thesis: the InternalRel of A -Seg x9 misses Y

per cases ( c in Y or not c in Y ) ;

suppose A42: 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 ;
A46: x99 < c by A5, A36, A39;
c <> x99 by A44, WELLORD1:1;
then c < x99 by A45;
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 ; :: 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 b₁ being object st
( b₁ in Y & the InternalRel of A -Seg b₁ 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 ;
the InternalRel of A is_antisymmetric_in the carrier of A by Def4;
then the InternalRel of A is_antisymmetric_in Z ;
then the InternalRel of A well_orders Z by A26, A49, A6, A28;
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