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, Th67;
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 set ; :: 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 set ; :: 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 ;
a in {a} by TARSKI:def 1;
then ( a1 < a & a1 in T ) by A4, A6, A7, XBOOLE_0:def 4;
then x in S by A1, A2, A6, Th70;
hence x in InitSegm S,a by A5, XBOOLE_0:def 4; :: thesis: verum