let k be Prime; :: thesis: not k is empty
assume k is empty ; :: thesis: contradiction
then k in SetPrimenumber 2 by NEWTON:def 7;
hence contradiction ; :: thesis: verum