set X = Seg n;
Seg n c= NAT

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Seg n or x in NAT )
assume x in Seg n ; :: thesis: x in NAT
then ex k being Element of NAT st
( x = k & 1 <= k & k <= n ) ;
hence x in NAT ; :: thesis: verum

end;

hence Seg n is Subset of NAT ; :: thesis: verum