for A being 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