let A be non empty Poset; :: thesis: for S being Subset of A holds
( S <> {} iff not S is Initial_Segm of S )
let S be Subset of A; :: thesis: ( S <> {} iff not S is Initial_Segm of S )
thus ( S <> {} implies not S is Initial_Segm of S ) :: thesis: ( S is not Initial_Segm of S implies S <> {} )

proof

assume ( S <> {} & S is Initial_Segm of S ) ; :: thesis: contradiction
then consider a being Element of A such that
A1: ( a in S & S = InitSegm (S,a) ) by Def11;
a in LowerCone {a} by A1, XBOOLE_0:def 4;
hence contradiction by Th21; :: thesis: verum

end;

thus ( S is not Initial_Segm of S implies S <> {} ) by Def11; :: thesis: verum