A1: {2,3,5,7,11} c= NAT
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {2,3,5,7,11} or x in NAT )
assume x in {2,3,5,7,11} ; :: thesis: x in NAT
then ( x = 2 or x = 3 or x = 5 or x = 7 or x = 11 ) by ENUMSET1:def 3;
hence x in NAT ; :: thesis: verum
end;
for q being Nat holds
( q in {2,3,5,7,11} iff ( q < 13 & q is prime ) )
proof
let q be Nat; :: thesis: ( q in {2,3,5,7,11} iff ( q < 13 & q is prime ) )
hereby :: thesis: ( q < 13 & q is prime implies q in {2,3,5,7,11} )
assume q in {2,3,5,7,11} ; :: thesis: ( q < 13 & q is prime )
then ( q = 2 or q = 3 or q = 5 or q = 7 or q = 11 ) by ENUMSET1:def 3;
hence ( q < 13 & q is prime ) by INT_2:28, PEPIN:41, PEPIN:59, NAT_4:26, NAT_4:27; :: thesis: verum
end;
assume Z: ( q < 13 & q is prime ) ; :: thesis: q in {2,3,5,7,11}
then q < 12 + 1 ;
then q <= 12 by NAT_1:13;
then not not q = 0 & ... & not q = 12 ;
hence q in {2,3,5,7,11} by ENUMSET1:def 3, Z, INT_2:29, lem6, lem8, lem9, lem12, lem10; :: thesis: verum
end;
hence SetPrimenumber 13 = {2,3,5,7,11} by A1, NEWTON:def 7; :: thesis: verum