:: deftheorem Def11 defines Initial_Segm ORDERS_2:def 11 :
for A being non empty Poset
for S, b₃ being Subset of A holds
( ( S <> {} implies ( b₃ is Initial_Segm of S iff ex a being Element of A st
( a in S & b₃ = InitSegm (S,a) ) ) ) & ( not S <> {} implies ( b₃ is Initial_Segm of S iff b₃ = {} ) ) );