0 + 1 is not Prime by INT_2:def 4;
then SetPrimes (0 + 1) = SetPrimes 0 by PrimesSet;
hence ( SetPrimes 0 = {} & SetPrimes 1 = {} ) ; :: thesis: verum