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;
( x < 2 & x is prime ) by A1, Def7;
then ( 0 is prime or 1 is prime ) by NAT_1:27;
hence contradiction by INT_2:def 5; :: thesis: verum