let A be non empty Poset; :: thesis: for f being Choice_Function of (BOOL the carrier of A)
for fC1, fC2 being Chain of f holds
( fC1 c< fC2 iff fC1 is Initial_Segm of fC2 )
let f be Choice_Function of (BOOL the carrier of A); :: thesis: for fC1, fC2 being Chain of f holds
( fC1 c< fC2 iff fC1 is Initial_Segm of fC2 )
let fC1, fC2 be Chain of f; :: thesis: ( fC1 c< fC2 iff fC1 is Initial_Segm of fC2 )
thus ( fC1 c< fC2 implies fC1 is Initial_Segm of fC2 ) :: thesis: ( fC1 is Initial_Segm of fC2 implies fC1 c< fC2 )
proof
assume A1: fC1 c< fC2 ; :: thesis: fC1 is Initial_Segm of fC2
now :: thesis: fC2 is not Initial_Segm of fC1
assume A2: fC2 is Initial_Segm of fC1 ; :: thesis: contradiction
fC1 <> {} by Def12;
then ex a being Element of A st
( a in fC1 & fC2 = InitSegm (fC1,a) ) by A2, Def11;
then fC2 c= fC1 by XBOOLE_1:17;
hence contradiction by A1, XBOOLE_0:def 8; :: thesis: verum
end;
hence fC1 is Initial_Segm of fC2 by A1, Th41; :: thesis: verum
end;
assume A3: fC1 is Initial_Segm of fC2 ; :: thesis: fC1 c< fC2
A4: fC2 <> {} by Def12;
then ex a being Element of A st
( a in fC2 & fC1 = InitSegm (fC2,a) ) by A3, Def11;
then A5: fC1 c= fC2 by XBOOLE_1:17;
fC1 <> fC2 by A3, A4, Th30;
hence fC1 c< fC2 by A5; :: thesis: verum