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 = {} )
assume A1: a = f . the carrier of A ; :: thesis: InitSegm fC,a = {}
then A2: a in fC by Th79;
consider x being Element of (LowerCone {a}) /\ fC;
assume A3: InitSegm fC,a <> {} ; :: thesis: contradiction
then A4: ( x in fC & fC c= the carrier of A ) by XBOOLE_0:def 4;
reconsider b = x as Element of A by A3, Lm1;
x in LowerCone {a} by A3, XBOOLE_0:def 4;
then A5: 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 ( a <= b & b < a ) by A1, A4, A5, Th80;
hence contradiction by A2, A4, Th39; :: thesis: verum