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

proof

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

end;

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