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