let A be non empty Poset; :: thesis: for S being Subset of A
for f being Choice_Function of BOOL the carrier of A
for fC being Chain of f st fC <> union (Chains f) & S = union (Chains f) holds
fC is Initial_Segm of S
let S be Subset of A; :: thesis: for f being Choice_Function of BOOL the carrier of A
for fC being Chain of f st fC <> union (Chains f) & S = union (Chains f) holds
fC is Initial_Segm of S
let f be Choice_Function of BOOL the carrier of A; :: thesis: for fC being Chain of f st fC <> union (Chains f) & S = union (Chains f) holds
fC is Initial_Segm of S
let fC be Chain of f; :: thesis: ( fC <> union (Chains f) & S = union (Chains f) implies fC is Initial_Segm of S )
assume that
A1: fC <> union (Chains f) and
A2: S = union (Chains f) ; :: thesis: fC is Initial_Segm of S
consider x being Element of S \ fC;
fC in Chains f by Def17;
then fC c= union (Chains f) by ZFMISC_1:92;
then not union (Chains f) c= fC by A1, XBOOLE_0:def 10;
then A3: S \ fC <> {} by A2, XBOOLE_1:37;
then x in S by XBOOLE_0:def 5;
then consider X being set such that
A4: x in X and
A5: X in Chains f by A2, TARSKI:def 4;
reconsider X = X as Chain of f by A5, Def17;
A6: not x in fC by A3, XBOOLE_0:def 5;
( fC <> X & not X c= fC ) by A3, A4, XBOOLE_0:def 5;
then not X c< fC by XBOOLE_0:def 8;
then X is not Initial_Segm of fC by Th84;
then ( fC is Initial_Segm of X & X <> {} ) by A4, A6, Th83;
then consider a being Element of A such that
A7: a in X and
A8: fC = InitSegm X,a by Def15;
A9: X c= S by A2, A5, ZFMISC_1:92;
InitSegm S,a = InitSegm X,a

proof

thus InitSegm S,a c= InitSegm X,a :: according to XBOOLE_0:def 10 :: thesis: InitSegm X,a c= InitSegm S,a

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in InitSegm S,a or x in InitSegm X,a )
assume A10: x in InitSegm S,a ; :: thesis: x in InitSegm X,a
then A11: x in LowerCone {a} by XBOOLE_0:def 4;
then consider b being Element of A such that
A12: b = x and
A13: for a2 being Element of A st a2 in {a} holds
b < a2 ;
a in {a} by TARSKI:def 1;
then A14: b < a by A13;
b in S by A10, A12, XBOOLE_0:def 4;
then consider Y being set such that
A15: b in Y and
A16: Y in Chains f by A2, TARSKI:def 4;
reconsider Y = Y as Chain of f by A16, Def17;

now

per cases ( X = Y or X <> Y ) ;

suppose X = Y ; :: thesis: x in InitSegm X,a

hence x in InitSegm X,a by A11, A12, A15, XBOOLE_0:def 4; :: thesis: verum

end;

suppose A17: X <> Y ; :: thesis: x in InitSegm X,a

now

per cases ( X is Initial_Segm of Y or Y is Initial_Segm of X ) by A17, Th83;

suppose X is Initial_Segm of Y ; :: thesis: x in InitSegm X,a

then x in X by A7, A12, A14, A15, Th70;
hence x in InitSegm X,a by A11, XBOOLE_0:def 4; :: thesis: verum

end;

suppose Y is Initial_Segm of X ; :: thesis: x in InitSegm X,a

then Y c< X by Th84;
then Y c= X by XBOOLE_0:def 8;
hence x in InitSegm X,a by A11, A12, A15, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

hence x in InitSegm X,a ; :: thesis: verum

end;

end;

end;

hence x in InitSegm X,a ; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in InitSegm X,a or x in InitSegm S,a )
assume x in InitSegm X,a ; :: thesis: x in InitSegm S,a
then ( x in LowerCone {a} & x in X ) by XBOOLE_0:def 4;
hence x in InitSegm S,a by A9, XBOOLE_0:def 4; :: thesis: verum

end;

hence fC is Initial_Segm of S by A7, A8, A9, Def15; :: thesis: verum