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; :: 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 ; :: 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 b₁ being object st
( b₁ in Y & the InternalRel of A -Seg b₁ misses Y ) )
set x = the Element of Y;
assume that
A6: Y c= C and
A7: Y <> {} ; :: thesis: ex b₁ being object st
( b₁ in Y & the InternalRel of A -Seg b₁ misses Y )
the Element of Y in C by A6, A7;
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 object such that
A11: a in X /\ Y and
A12: for x being object 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 object ; :: 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 ;

now :: thesis: y in X

per cases ( X <> C or X = C ) ;

suppose A18: X <> C ; :: thesis: y in X

( a in X & b < aa ) by A11, A16, A17, 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 ;
hence y in {} by A16, A17, Th2; :: thesis: verum

end;

thus {} c= ( the InternalRel of A -Seg a) /\ Y ; :: thesis: verum

end;

C <> {} by Th43;
hence union (Chains f) is Chain of f by A4, A1, Def12; :: thesis: verum