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 <> {} ) by Def12;
then consider x being object such that
A3: x in fC and
A4: 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 A3;

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

set y = the Element of (LowerCone {x}) /\ fC;
assume A6: (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 A6, 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 ) ) ;
the Element of (LowerCone {x}) /\ fC in fC by A6, XBOOLE_0:def 4;
then [x, the Element of (LowerCone {x}) /\ fC] in the InternalRel of A by A4;
then A8: x <= a ;
x in {x} by TARSKI:def 1;
hence contradiction by A8, A7, Th6; :: thesis: verum

end;

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