0 = card (SetPrimenumber 2) ;
hence primenumber 0 = 2 by INT_2:28, NEWTON:def 8; :: thesis: verum