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: C <> {} by Th87;
A2: the InternalRel of A well_orders C

proof

( the InternalRel of A is_reflexive_in the carrier of A & the InternalRel of A is_transitive_in the carrier of A & the InternalRel of A is_antisymmetric_in the carrier of A ) by Def4, Def5, Def6;
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 ORDERS_1:93, ORDERS_1:94, ORDERS_1:95; :: 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 Def11;
hence the InternalRel of A is_connected_in C by ORDERS_1:92; :: 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 set st
( b₁ in Y & the InternalRel of A -Seg b₁ misses Y ) )
consider x being Element of Y;
assume that
A3: Y c= C and
A4: Y <> {} ; :: thesis: ex b₁ being set st
( b₁ in Y & the InternalRel of A -Seg b₁ misses Y )
x in C by A3, A4, TARSKI:def 3;
then consider X being set such that
A5: x in X and
A6: X in Chains f by TARSKI:def 4;
reconsider X = X as Chain of f by A6, Def17;
( X /\ Y <> {} & X /\ Y c= X & the InternalRel of A well_orders X ) by A4, A5, Def16, XBOOLE_0:def 4, XBOOLE_1:17;
then consider a being set such that
A7: a in X /\ Y and
A8: for x being set st x in X /\ Y holds
[a,x] in the InternalRel of A by WELLORD1:9;
reconsider aa = a as Element of A by A7;
take a ; :: thesis: ( a in Y & the InternalRel of A -Seg a misses Y )
thus a in Y by A7, XBOOLE_0:def 4; :: thesis: the InternalRel of A -Seg a misses Y
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 y in (the InternalRel of A -Seg a) /\ Y ; :: thesis: y in {}
then A9: ( y in Y & y in the InternalRel of A -Seg a ) by XBOOLE_0:def 4;
then ( y in C & C c= the carrier of A ) by A3;
then reconsider b = y as Element of A ;
A10: ( y <> a & [y,a] in the InternalRel of A ) by A9, WELLORD1:def 1;
then A11: b <= aa by Def9;

now

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

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

then ( a in X & b < aa & X is Initial_Segm of C & y in C ) by A3, A7, A9, A10, A11, Def10, Th88, XBOOLE_0:def 4;
hence y in X by Th70; :: thesis: verum

end;

suppose X = C ; :: thesis: y in X

hence y in X by A3, A9; :: thesis: verum

end;

end;

end;

then y in X /\ Y by A9, XBOOLE_0:def 4;
then [a,y] in the InternalRel of A by A8;
then aa <= b by Def9;
hence y in {} by A10, A11, Th25; :: thesis: verum

end;

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

end;

now

let a be Element of A; :: thesis: ( a in C implies f . (UpperCone (InitSegm C,a)) = a )
assume A12: a in C ; :: thesis: f . (UpperCone (InitSegm C,a)) = a
then consider X being set such that
A13: a in X and
A14: X in Chains f by TARSKI:def 4;
reconsider X = X as Chain of f by A14, Def17;

now

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

suppose X = C ; :: thesis: f . (UpperCone (InitSegm C,a)) = a

hence f . (UpperCone (InitSegm C,a)) = a by A12, Def16; :: thesis: verum

end;

suppose X <> C ; :: thesis: f . (UpperCone (InitSegm C,a)) = a

then X is Initial_Segm of C by Th88;
then ( InitSegm C,a = InitSegm X,a & f . (UpperCone (InitSegm X,a)) = a ) by A13, Def16, Th71;
hence f . (UpperCone (InitSegm C,a)) = a ; :: thesis: verum

end;

end;

end;

hence f . (UpperCone (InitSegm C,a)) = a ; :: thesis: verum

end;

hence union (Chains f) is Chain of f by A1, A2, Def16; :: thesis: verum