let S be Subset of NAT; :: thesis: ( S = SegM n iff S = { k where k is Nat : k <= n } )
SegM (Segm n) = { k where k is Nat : k <= n } by NAT_1:54;
hence ( S = SegM n iff S = { k where k is Nat : k <= n } ) ; :: thesis: verum