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

assume k is zero ; :: thesis: contradiction

then k in SetPrimenumber 2 by NEWTON:def 7;

hence contradiction ; :: thesis: verum