let A be non empty Poset; 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; 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; ( S c= T implies InitSegm (S,a) c= InitSegm (T,a) )
assume A1:
S c= T
; InitSegm (S,a) c= InitSegm (T,a)
let x be object ; TARSKI:def 3 ( not x in InitSegm (S,a) or x in InitSegm (T,a) )
assume
x in InitSegm (S,a)
; 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; verum