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 <> {} ) by Def12;
then consider x being object such that
A1: x in fC and
A2: for y being object st y in fC holds
[x,y] in the InternalRel of A by WELLORD1:5;
reconsider x = x as Element of A by A1;

A3: now :: thesis: not (LowerCone {x}) /\ fC <> {} A

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

end;

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