assume SetPrimenumber 2 <> {} ; :: thesis: contradiction
then consider x being set 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 < 2 by A1, Def7;
then ( 0 is prime or 1 is prime ) by A2, NAT_1:26;
hence contradiction by INT_2:def 4; :: thesis: verum