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 )
consider f being Choice_Function of BOOL the carrier of A;
reconsider F = union (Chains f) as Chain of f by Th89;
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

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, Th32; :: 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:4;
then A4: f . (UpperCone F) in UpperCone F by A3, ORDERS_1:def 1;
then reconsider c = f . (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 b₁ being set holds
( not x in Z or not b₁ in Z or x = b₁ or [x,b₁] in the InternalRel of A or [b₁,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

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 Th38;
hence ( x = y or [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by Def9; :: 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 by Def10;
hence ( x = y or [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by Def9; :: 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 by Def10;
hence ( x = y or [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by Def9; :: 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

let a1 be Element of A; :: thesis: ( a1 in Z implies f . (UpperCone (InitSegm Z,a1)) = a1 )
assume A12: a1 in Z ; :: thesis: f . (UpperCone (InitSegm Z,a1)) = a1

now

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

suppose A13: a1 = c ; :: thesis: f . (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, Th50; :: 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 Th52;
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 f . (UpperCone (InitSegm Z,a1)) = a1 by A13; :: thesis: verum

end;

suppose a1 <> c ; :: thesis: f . (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

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, Th28; :: 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 Th65, XBOOLE_1:7;
then InitSegm Z,a1 = InitSegm F,a1 by A20, XBOOLE_0:def 10;
hence f . (UpperCone (InitSegm Z,a1)) = a1 by A19, Def16; :: thesis: verum

end;

end;

end;

hence f . (UpperCone (InitSegm Z,a1)) = a1 ; :: thesis: verum

end;

the InternalRel of A is_reflexive_in the carrier of A by Def4;
then A26: the InternalRel of A is_reflexive_in Z by ORDERS_1:93;
then the InternalRel of A is_strongly_connected_in Z by A6, ORDERS_1:92;
then A27: Z is Chain of A by Def11;
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 set 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 set st
( b₁ in Y & the InternalRel of A -Seg b₁ misses Y )

now

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 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:def 1; :: thesis: verum

end;

case A34: 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

assume Y \ {c} = {} ; :: thesis: contradiction
then Y c= {c} by XBOOLE_1:37;
hence contradiction by A30, A34, ZFMISC_1:39; :: 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 Def16;
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

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

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:def 1;
then A45: c <= x99 by Def9;
A46: x99 < c by A5, A36, A39;
c <> x99 by A44, WELLORD1:def 1;
then c < x99 by A45, Def10;
hence contradiction by A46, Th28; :: thesis: verum

end;

A47: now

consider x being Element of (the InternalRel of A -Seg x9) /\ {c};
assume A48: (the InternalRel of A -Seg x9) /\ {c} <> {} ; :: thesis: contradiction
then x in {c} by XBOOLE_0:def 4;
then x = c by TARSKI:def 1;
hence contradiction by A43, A48, XBOOLE_0:def 4; :: thesis: verum

end;

{c} c= Y by A42, ZFMISC_1:37;
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:56;
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 set 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 Def5;
then A49: the InternalRel of A is_transitive_in Z by ORDERS_1:95;
the InternalRel of A is_antisymmetric_in the carrier of A by Def6;
then the InternalRel of A is_antisymmetric_in Z by ORDERS_1:94;
then the InternalRel of A well_orders Z by A26, A49, A6, A28, WELLORD1:def 5;
then reconsider Z = Z as Chain of f by A27, A11, Def16;
c in {c} by TARSKI:def 1;
then A50: c in Z by XBOOLE_0:def 3;
Z in Chains f by Def17;
then c in F by A50, TARSKI:def 4;
hence contradiction by A5; :: thesis: verum