theorem Th30: :: ORDERS_2:30

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