assume SetPrimenumber 2 <> {} ; :: thesis: contradiction
then consider x being object such that
A1: x in SetPrimenumber 2 by XBOOLE_0:def 1;
reconsider x = x as Nat by A1;
A2: x is prime by A1, Def7;
x < 1 + 1 by A1, Def7;
then x <= 1 by NAT_1:13;
then ( 0 is prime or 1 is prime ) by A2, NAT_1:25;
hence contradiction by INT_2:def 4; :: thesis: verum