let A be non empty Poset; :: thesis: for a being Element of A
for S, T being Subset of A st a in S & S is Initial_Segm of T holds
InitSegm (S,a) = InitSegm (T,a)
let a be Element of A; :: thesis: for S, T being Subset of A st a in S & S is Initial_Segm of T holds
InitSegm (S,a) = InitSegm (T,a)
let S, T be Subset of A; :: thesis: ( a in S & S is Initial_Segm of T implies InitSegm (S,a) = InitSegm (T,a) )
assume that
A1: a in S and
A2: S is Initial_Segm of T ; :: thesis: InitSegm (S,a) = InitSegm (T,a)
A3: S c= T by A2, Th29;
thus InitSegm (S,a) c= InitSegm (T,a) :: according to XBOOLE_0:def 10 :: thesis: InitSegm (T,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 (T,a) )
assume x in InitSegm (S,a) ; :: thesis: x in InitSegm (T,a)
then ( x in LowerCone {a} & x in S ) by XBOOLE_0:def 4;
hence x in InitSegm (T,a) by A3, XBOOLE_0:def 4; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in InitSegm (T,a) or x in InitSegm (S,a) )
assume A4: x in InitSegm (T,a) ; :: thesis: x in InitSegm (S,a)
then A5: x in LowerCone {a} by XBOOLE_0:def 4;
then consider a1 being Element of A such that
A6: x = a1 and
A7: for a2 being Element of A st a2 in {a} holds
a1 < a2 ;
A8: a1 in T by A4, A6, XBOOLE_0:def 4;
a in {a} by TARSKI:def 1;
then a1 < a by A7;
then x in S by A1, A2, A6, A8, Th32;
hence x in InitSegm (S,a) by A5, XBOOLE_0:def 4; :: thesis: verum