let A be non empty Poset; :: thesis: for a being Element of A
for S, T being Subset of A st S c= T holds
InitSegm (S,a) c= InitSegm (T,a)
let a be Element of A; :: thesis: for S, T being Subset of A st S c= T holds
InitSegm (S,a) c= InitSegm (T,a)
let S, T be Subset of A; :: thesis: ( S c= T implies InitSegm (S,a) c= InitSegm (T,a) )
assume A1: S c= T ; :: thesis: InitSegm (S,a) c= InitSegm (T,a)
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 S & x in LowerCone {a} ) by XBOOLE_0:def 4;
hence x in InitSegm (T,a) by A1, XBOOLE_0:def 4; :: thesis: verum