for A being non empty Poset
for a being Element of A
for S, T being Subset of A st a in S & S is Initial_Segm of T holds
InitSegm (S,a) = InitSegm (T,a)