for A being non empty Poset
for S being Subset of A
for I being Initial_Segm of S holds I c= S