set X = { k where k is Element of NAT : 5 <= k } ;
{ k where k is Element of NAT : 5 <= k } c= NAT

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { k where k is Element of NAT : 5 <= k } or a in NAT )
assume a in { k where k is Element of NAT : 5 <= k } ; :: thesis: a in NAT
then ex k being Element of NAT st
( a = k & 5 <= k ) ;
hence a in NAT ; :: thesis: verum

end;

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