1 = card (SetPrimenumber 3) by LS2, CARD_2:42;
hence primenumber 1 = 3 by PEPIN:41, NEWTON:def 8; :: thesis: verum