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
set x = the Element of S \ fC;
fC in Chains f by Def13;
then fC c= union (Chains f) by ZFMISC_1:74;
then not union (Chains f) c= fC by A1;
then A3: S \ fC <> {} by A2, XBOOLE_1:37;
then A4: not the Element of S \ fC in fC by XBOOLE_0:def 5;
the Element of S \ fC in S by A3, XBOOLE_0:def 5;
then consider X being set such that
A5: the Element of S \ fC in X and
A6: X in Chains f by A2, TARSKI:def 4;
reconsider X = X as Chain of f by A6, Def13;
not X c= fC by A3, A5, XBOOLE_0:def 5;
then not X c< fC ;
then X is not Initial_Segm of fC by Th42;
then fC is Initial_Segm of X by A5, A4, Th41;
then consider a being Element of A such that
A7: a in X and
A8: fC = InitSegm (X,a) by A5, Def11;
A9: X c= S by A2, A6, ZFMISC_1:74;
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 object ; :: 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 ;
b in S by A10, A12, XBOOLE_0:def 4;
then consider Y being set such that
A14: b in Y and
A15: Y in Chains f by A2, TARSKI:def 4;
reconsider Y = Y as Chain of f by A15, Def13;
a in {a} by TARSKI:def 1;
then A16: b < a by A13;

now :: thesis: x in InitSegm (X,a)

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, A14, XBOOLE_0:def 4; :: thesis: verum

end;

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

now :: thesis: x in InitSegm (X,a)

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

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

then x in X by A7, A12, A16, A14, Th32;
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 Th42;
then Y c= X ;
hence x in InitSegm (X,a) by A11, A12, A14, 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 object ; :: 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, Def11; :: thesis: verum