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 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 S & x in LowerCone {a} ) by XBOOLE_0:def 4;
hence x in InitSegm T,a by A1, XBOOLE_0:def 4; :: thesis: verum