set X = { k where k is Element of NAT : k <= n } ;
0 <= n by NAT_1:2;
then 0 in { k where k is Element of NAT : k <= n } ;
then reconsider X = { k where k is Element of NAT : k <= n } as non empty set ;
X c= NAT

proof

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

end;

hence { k where k is Element of NAT : k <= n } is Subset of NAT ; :: thesis: verum