A1: {2,3} is Subset of NAT by ZFMISC_1:32;
for q being Nat holds
( q in {2,3} iff ( q < 5 & q is prime ) )
proof
let q be Nat; :: thesis: ( q in {2,3} iff ( q < 5 & q is prime ) )
hereby :: thesis: ( q < 5 & q is prime implies q in {2,3} )
assume q in {2,3} ; :: thesis: ( q < 5 & q is prime )
then ( q = 2 or q = 3 ) by TARSKI:def 2;
hence ( q < 5 & q is prime ) by INT_2:28, PEPIN:41; :: thesis: verum
end;
assume Z: ( q < 5 & q is prime ) ; :: thesis: q in {2,3}
then q < 4 + 1 ;
then q <= 4 by NAT_1:13;
then not not q = 0 & ... & not q = 4 ;
hence q in {2,3} by TARSKI:def 2, Z, INT_2:29; :: thesis: verum
end;
hence SetPrimenumber 5 = {2,3} by A1, NEWTON:def 7; :: thesis: verum