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 )
assume A1: 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
consider f being Choice_Function of BOOL the carrier of A;
reconsider F = union (Chains f) as Chain of f by Th89;
consider a being Element of A such that
A2: for b being Element of A st b in F holds
b <= a by A1;
take a ; :: thesis: for b being Element of A holds not a < b
let b be Element of A; :: thesis: not a < b
assume A3: 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 A2;
hence a1 < b by A3, 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 ( UpperCone F in BOOL the carrier of A & not {} in BOOL the carrier of A ) by ORDERS_1:4, XBOOLE_0:def 5;
then A4: f . (UpperCone F) in UpperCone F by ORDERS_1:def 1;
then reconsider c = f . (UpperCone F) as Element 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;
reconsider Z = F \/ {c} as Subset of A ;
( Z c= the carrier of A & the InternalRel of A is_reflexive_in the carrier of A & the InternalRel of A is_antisymmetric_in the carrier of A & the InternalRel of A is_transitive_in the carrier of A ) by Def4, Def5, Def6;
then A6: ( the InternalRel of A is_reflexive_in Z & the InternalRel of A is_antisymmetric_in Z & the InternalRel of A is_transitive_in Z ) by ORDERS_1:93, ORDERS_1:94, ORDERS_1:95;
A7: 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 that
A8: x in Z and
A9: y in Z ; :: thesis: ( x = y or [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
reconsider x1 = x, y1 = y as Element of A by A8, A9;

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 A8, A9, 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 ( 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 ( x1 in F & y1 = c ) by TARSKI:def 1;
then x1 < y1 by A5;
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 ( 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 ( y1 in F & x1 = c ) by TARSKI:def 1;
then y1 < x1 by A5;
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 ( 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 ( c <= c & x1 = c & y1 = c ) by TARSKI:def 1;
hence ( x = y or [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) ; :: 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;

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
A10: Y c= Z and
A11: 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 A12: 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 A12, 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 x' being set such that
A13: ( x' in the InternalRel of A -Seg x & x' in Y ) by XBOOLE_0:3;
( x' = c & x' in the InternalRel of A -Seg x ) by A12, A13, TARSKI:def 1;
hence contradiction by WELLORD1:def 1; :: thesis: verum

end;

case A14: Y <> {c} ; :: thesis: ex x' being set st
( x' in Y & the InternalRel of A -Seg x' misses Y )

set X = Y \ {c};
A15: 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
A16: x in Y \ {c} and
A17: not x in F ; :: thesis: contradiction
x in Y by A16;
then ( x in {c} & not x in {c} ) by A10, A16, A17, XBOOLE_0:def 3, XBOOLE_0:def 5;
hence contradiction ; :: thesis: verum

end;

the InternalRel of A well_orders F by Def16;
then the InternalRel of A well_orders Y \ {c} by A15, Lm5;
then A18: the InternalRel of A is_well_founded_in Y \ {c} by WELLORD1:def 5;

now

assume Y \ {c} = {} ; :: thesis: contradiction
then Y c= {c} by XBOOLE_1:37;
hence contradiction by A11, A14, ZFMISC_1:39; :: thesis: verum

end;

then consider x being set such that
A19: x in Y \ {c} and
A20: the InternalRel of A -Seg x misses Y \ {c} by A18, WELLORD1:def 3;
A21: (the InternalRel of A -Seg x) /\ (Y \ {c}) = {} by A20, XBOOLE_0:def 7;
take x' = x; :: thesis: ( x' in Y & the InternalRel of A -Seg x' misses Y )
thus x' in Y by A19; :: thesis: the InternalRel of A -Seg x' misses Y

now

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

suppose c in Y ; :: thesis: the InternalRel of A -Seg x' misses Y

then {c} c= Y by ZFMISC_1:37;
then A22: Y = (Y \ {c}) \/ {c} by XBOOLE_1:45;

A23: now

assume c in the InternalRel of A -Seg x' ; :: thesis: contradiction
then A24: ( c <> x' & [c,x'] in the InternalRel of A ) by WELLORD1:def 1;
x' in F by A15, A19;
then reconsider x'' = x' as Element of A ;
( c <> x'' & c <= x'' ) by A24, Def9;
then ( c < x'' & x'' < c ) by A5, A15, A19, Def10;
hence contradiction by Th28; :: thesis: verum

end;

now

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

end;

then (the InternalRel of A -Seg x') /\ Y = {} \/ {} by A21, A22, XBOOLE_1:23
.= {} ;
hence the InternalRel of A -Seg x' misses Y by XBOOLE_0:def 7; :: thesis: verum

end;

suppose not c in Y ; :: thesis: the InternalRel of A -Seg x' misses Y

then Y misses {c} by ZFMISC_1:56;
hence the InternalRel of A -Seg x' misses Y by A20, XBOOLE_1:83; :: thesis: verum

end;

end;

end;

hence the InternalRel of A -Seg x' 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;

then A26: the InternalRel of A well_orders Z by A6, A7, WELLORD1:def 5;
the InternalRel of A is_strongly_connected_in Z by A6, A7, ORDERS_1:92;
then A27: Z is Chain of A by Def11;

now

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

now

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

suppose A29: 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
A30: x in InitSegm Z,c and
A31: not x in F ; :: thesis: contradiction
x in Z by A30, XBOOLE_0:def 4;
then x in {c} by A31, XBOOLE_0:def 3;
then ( x = c & x in LowerCone {c} ) by A30, TARSKI:def 1, XBOOLE_0:def 4;
hence contradiction by 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 A32: x in F ; :: thesis: x in InitSegm Z,c
then A33: x in Z by XBOOLE_0:def 3;
reconsider y = x as Element of A by A32;
y < c by A5, A32;
then x in LowerCone {c} by Th52;
hence x in InitSegm Z,c by A33, XBOOLE_0:def 4; :: thesis: verum

end;

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

end;

suppose a1 <> c ; :: thesis: f . (UpperCone (InitSegm Z,a1)) = a1

then not a1 in {c} by TARSKI:def 1;
then A34: a1 in F by A28, XBOOLE_0:def 3;
InitSegm Z,a1 = InitSegm F,a1

proof

thus InitSegm Z,a1 c= InitSegm F,a1 :: according to XBOOLE_0:def 10 :: thesis: InitSegm F,a1 c= InitSegm Z,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 A35: x in InitSegm Z,a1 ; :: thesis: x in InitSegm F,a1
then A36: x in LowerCone {a1} by XBOOLE_0:def 4;

now

assume A37: not x in F ; :: thesis: contradiction
x in Z by A35, XBOOLE_0:def 4;
then x in {c} by A37, XBOOLE_0:def 3;
then x = c by TARSKI:def 1;
then A38: ex c1 being Element of A st
( c1 = c & ( for c2 being Element of A st c2 in {a1} holds
c1 < c2 ) ) by A36;
a1 in {a1} by TARSKI:def 1;
then ( c < a1 & a1 < c ) by A5, A34, A38;
hence contradiction by Th28; :: thesis: verum

end;

hence x in InitSegm F,a1 by A36, XBOOLE_0:def 4; :: thesis: verum

end;

thus InitSegm F,a1 c= InitSegm Z,a1 by Th65, XBOOLE_1:7; :: thesis: verum

end;

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

end;

end;

end;

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

end;

then reconsider Z = Z as Chain of f by A26, A27, Def16;
c in {c} by TARSKI:def 1;
then ( Z in Chains f & c in Z ) by Def17, XBOOLE_0:def 3;
then c in F by TARSKI:def 4;
hence contradiction by A5; :: thesis: verum