let X be set ; :: thesis: ( X is included_in_Seg implies ( Sgm X = {} iff X = {} ) )
assume X is included_in_Seg ; :: thesis: ( Sgm X = {} iff X = {} )
then rng (Sgm X) = X by Def13;
hence ( Sgm X = {} iff X = {} ) ; :: thesis: verum