let A be non empty Poset; :: thesis: for f being Choice_Function of BOOL the carrier of A
for fC being Chain of f holds f . the carrier of A in fC
let f be Choice_Function of BOOL the carrier of A; :: thesis: for fC being Chain of f holds f . the carrier of A in fC
let fC be Chain of f; :: thesis: f . the carrier of A in fC
( the InternalRel of A well_orders fC & fC <> {} & fC c= fC ) by Def16;
then consider x being set such that
A1: x in fC and
A2: for y being set st y in fC holds
[x,y] in the InternalRel of A by WELLORD1:9;
reconsider x = x as Element of A by A1;

A3: now

consider y being Element of (LowerCone {x}) /\ fC;
assume A4: (LowerCone {x}) /\ fC <> {} A ; :: thesis: contradiction
then A5: y in fC by XBOOLE_0:def 4;
reconsider a = y as Element of A by A4, Lm1;
[x,y] in the InternalRel of A by A2, A5;
then A6: x <= a by Def9;
a in LowerCone {x} by A4, XBOOLE_0:def 4;
then A7: ex a1 being Element of A st
( a = a1 & ( for a2 being Element of A st a2 in {x} holds
a1 < a2 ) ) ;
x in {x} by TARSKI:def 1;
hence contradiction by A6, A7, Th30; :: thesis: verum

end;

(LowerCone {x}) /\ fC = InitSegm fC,x ;
then f . (UpperCone ((LowerCone {x}) /\ fC)) = x by A1, Def16;
hence f . the carrier of A in fC by A1, A3, Th43; :: thesis: verum