set A = { a where a is Nat : a <= (6 * n) + 1 } ;
{ a where a is Nat : a <= (6 * n) + 1 } c= NAT

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { a where a is Nat : a <= (6 * n) + 1 } or x in NAT )
assume x in { a where a is Nat : a <= (6 * n) + 1 } ; :: thesis: x in NAT
then ex a being Nat st
( x = a & a <= (6 * n) + 1 ) ;
hence x in NAT by ORDINAL1:def 12; :: thesis: verum

end;

hence { a where a is Nat : a <= (6 * n) + 1 } is Subset of NAT ; :: thesis: verum