A1: {2} is Subset of NAT by ZFMISC_1:31;
for q being Nat holds
( q in {2} iff ( q < 3 & q is prime ) )

proof

let q be Nat; :: thesis: ( q in {2} iff ( q < 3 & q is prime ) )

hereby :: thesis: ( q < 3 & q is prime implies q in {2} )

assume q in {2} ; :: thesis: ( q < 3 & q is prime )
then q = 2 by TARSKI:def 1;
hence ( q < 3 & q is prime ) by INT_2:28; :: thesis: verum

end;

assume Z: ( q < 3 & q is prime ) ; :: thesis: q in {2}
then q < 2 + 1 ;
then q <= 2 by NAT_1:13;
then not not q = 0 & ... & not q = 2 ;
hence q in {2} by TARSKI:def 1, Z; :: thesis: verum

end;

hence SetPrimenumber 3 = {2} by A1, NEWTON:def 7; :: thesis: verum