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

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
A3: a in X and
A4: X in Chains f by TARSKI:def 4;
reconsider X = X as Chain of f by A4, Def17;

now

InitSegm C,a = InitSegm X,a by A3, Th71, Th88;
hence f . (UpperCone (InitSegm C,a)) = a by A3, Def16; :: thesis: verum

end;

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

end;

A5: the InternalRel of A well_orders C

proof

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

now

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

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

( a in X & b < aa ) by A12, A17, A18, Def10, XBOOLE_0:def 4;
hence y in X by A7, A15, A19, Th70, Th88; :: thesis: verum

end;

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

hence y in X by A7, A15; :: thesis: verum

end;

end;

end;

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

end;

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

end;

C <> {} by Th87;
hence union (Chains f) is Chain of f by A5, A1, Def16; :: thesis: verum