let A be non empty Poset; :: thesis: for f being Choice_Function of BOOL the carrier of A holds {(f . the carrier of A)} is Chain of f
let f be Choice_Function of BOOL the carrier of A; :: thesis: {(f . the carrier of A)} is Chain of f
set AC = the carrier of A;
( the carrier of A in BOOL the carrier of A & not {} in BOOL the carrier of A ) by ORDERS_1:4, ORDERS_1:5;
then reconsider aa = f . the carrier of A as Element of A by ORDERS_1:def 1;
reconsider X = {aa} as Chain of A by Th35;
( X c= the carrier of A & 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;
then A1: ( the InternalRel of A is_reflexive_in X & the InternalRel of A is_transitive_in X & the InternalRel of A is_antisymmetric_in X ) by ORDERS_1:93, ORDERS_1:94, ORDERS_1:95;
the InternalRel of A is_strongly_connected_in X by Def11;
then A2: the InternalRel of A is_connected_in X by ORDERS_1:92;
the InternalRel of A is_well_founded_in X

proof

let Y be set ; :: according to WELLORD1:def 3 :: thesis: ( not Y c= X or Y = {} or ex b₁ being set st
( b₁ in Y & the InternalRel of A -Seg b₁ misses Y ) )
assume that
A3: Y c= X and
A4: Y <> {} ; :: thesis: ex b₁ being set st
( b₁ in Y & the InternalRel of A -Seg b₁ misses Y )
reconsider x = aa as set ;
take x ; :: thesis: ( x in Y & the InternalRel of A -Seg x misses Y )
Y = X by A3, A4, ZFMISC_1:39;
hence x in Y by TARSKI:def 1; :: thesis: the InternalRel of A -Seg x misses Y
thus (the InternalRel of A -Seg x) /\ Y c= {} :: according to XBOOLE_0:def 7,XBOOLE_0:def 10 :: thesis: {} c= (the InternalRel of A -Seg x) /\ Y

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in (the InternalRel of A -Seg x) /\ Y or y in {} )
assume A5: y in (the InternalRel of A -Seg x) /\ Y ; :: thesis: y in {}
then y in Y by XBOOLE_0:def 4;
then A6: y = aa by A3, TARSKI:def 1;
y in the InternalRel of A -Seg x by A5, XBOOLE_0:def 4;
hence y in {} by A6, WELLORD1:def 1; :: thesis: verum

end;

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

end;

then A7: the InternalRel of A well_orders X by A1, A2, WELLORD1:def 5;
for a being Element of A st a in X holds
f . (UpperCone (InitSegm X,a)) = a

proof

let a be Element of A; :: thesis: ( a in X implies f . (UpperCone (InitSegm X,a)) = a )
assume a in X ; :: thesis: f . (UpperCone (InitSegm X,a)) = a
then A8: a = aa by TARSKI:def 1;
(LowerCone {a}) /\ X = {} A

proof

thus (LowerCone {a}) /\ X c= {} A :: according to XBOOLE_0:def 10 :: thesis: {} A c= (LowerCone {a}) /\ X

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (LowerCone {a}) /\ X or x in {} A )
assume A9: x in (LowerCone {a}) /\ X ; :: thesis: x in {} A
then A10: x in X by XBOOLE_0:def 4;
x in LowerCone {a} by A9, XBOOLE_0:def 4;
then consider a1 being Element of A such that
A11: x = a1 and
A12: for a2 being Element of A st a2 in {a} holds
a1 < a2 ;
thus x in {} A by A8, A10, A11, A12; :: thesis: verum

end;

thus {} A c= (LowerCone {a}) /\ X by XBOOLE_1:2; :: thesis: verum

end;

hence f . (UpperCone (InitSegm X,a)) = a by A8, Th43; :: thesis: verum

end;

hence {(f . the carrier of A)} is Chain of f by A7, Def16; :: thesis: verum