for A being non empty Poset
for S being Subset of A holds
( S <> {} iff not S is Initial_Segm of S )