let A be non empty Poset; :: thesis: for a being Element of A
for f being Choice_Function of (BOOL the carrier of A)
for fC being Chain of f st a = f . the carrier of A holds
InitSegm (fC,a) = {}
let a be Element of A; :: thesis: for f being Choice_Function of (BOOL the carrier of A)
for fC being Chain of f st a = f . the carrier of A holds
InitSegm (fC,a) = {}
let f be Choice_Function of (BOOL the carrier of A); :: thesis: for fC being Chain of f st a = f . the carrier of A holds
InitSegm (fC,a) = {}
let fC be Chain of f; :: thesis: ( a = f . the carrier of A implies InitSegm (fC,a) = {} )
set x = the Element of (LowerCone {a}) /\ fC;
assume A1: a = f . the carrier of A ; :: thesis: InitSegm (fC,a) = {}
then A2: a in fC by Th37;
assume A3: InitSegm (fC,a) <> {} ; :: thesis: contradiction
then reconsider b = the Element of (LowerCone {a}) /\ fC as Element of A by Lm1;
the Element of (LowerCone {a}) /\ fC in LowerCone {a} by A3, XBOOLE_0:def 4;
then A4: ex a1 being Element of A st
( a1 = b & ( for a2 being Element of A st a2 in {a} holds
a1 < a2 ) ) ;
a in {a} by TARSKI:def 1;
then A5: b < a by A4;
A6: the Element of (LowerCone {a}) /\ fC in fC by A3, XBOOLE_0:def 4;
then a <= b by A1, Th38;
hence contradiction by A2, A6, A5, Th12; :: thesis: verum