let A be non empty Poset; for a1, a2 being Element of A
for S, T being Subset of A st a1 < a2 & a1 in S & a2 in T & T is Initial_Segm of S holds
a1 in T
let a1, a2 be Element of A; for S, T being Subset of A st a1 < a2 & a1 in S & a2 in T & T is Initial_Segm of S holds
a1 in T
let S, T be Subset of A; ( a1 < a2 & a1 in S & a2 in T & T is Initial_Segm of S implies a1 in T )
assume that
A1:
a1 < a2
and
A2:
a1 in S
and
A3:
a2 in T
and
A4:
T is Initial_Segm of S
; a1 in T
consider a being Element of A such that
a in S
and
A5:
T = InitSegm (S,a)
by A2, A4, Def11;
then
a1 in LowerCone {a}
;
hence
a1 in T
by A2, A5, XBOOLE_0:def 4; verum