let X be set ; :: thesis: ( ex k being Nat st X c= Seg k implies ( Sgm X = {} iff X = {} ) )
given k being Nat such that A1: X c= Seg k ; :: thesis: ( Sgm X = {} iff X = {} )
thus ( Sgm X = {} implies X = {} ) :: thesis: ( X = {} implies Sgm X = {} )

proof

assume Sgm X = {} ; :: thesis: X = {}
hence X = rng {} by A1, Def13
.= {} ;
:: thesis: verum

end;

assume X = {} ; :: thesis: Sgm X = {}
then rng (Sgm X) = {} by A1, Def13;
hence Sgm X = {} ; :: thesis: verum