let A be non empty Poset; :: thesis: for a, b being Element of A
for f being Choice_Function of BOOL the carrier of A
for fC being Chain of f st a in fC & b = f . the carrier of A holds
b <= a
let a, b be Element of A; :: thesis: for f being Choice_Function of BOOL the carrier of A
for fC being Chain of f st a in fC & b = f . the carrier of A holds
b <= a
let f be Choice_Function of BOOL the carrier of A; :: thesis: for fC being Chain of f st a in fC & b = f . the carrier of A holds
b <= a
let fC be Chain of f; :: thesis: ( a in fC & b = f . the carrier of A implies b <= a )
assume that
A1: a in fC and
A2: b = f . the carrier of A ; :: thesis: b <= a
( the InternalRel of A well_orders fC & fC <> {} & fC c= fC ) by Def16;
then consider x being set such that
A3: x in fC and
A4: 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 A3;

A5: now

consider y being Element of (LowerCone {x}) /\ fC;
assume A6: (LowerCone {x}) /\ fC <> {} A ; :: thesis: contradiction
then A7: y in fC by XBOOLE_0:def 4;
reconsider a = y as Element of A by A6, Lm1;
[x,y] in the InternalRel of A by A4, A7;
then A8: x <= a by Def9;
a in LowerCone {x} by A6, XBOOLE_0:def 4;
then A9: 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 A8, A9, Th30; :: thesis: verum

end;

(LowerCone {x}) /\ fC = InitSegm fC,x ;
then f . (UpperCone ((LowerCone {x}) /\ fC)) = x by A3, Def16;
then A10: f . the carrier of A = x by A5, Th43;
[x,a] in the InternalRel of A by A1, A4;
hence b <= a by A2, A10, Def9; :: thesis: verum