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