3 = card (SetPrimenumber 7) by LS4, CARD_2:58;
hence primenumber 3 = 7 by NAT_4:26, NEWTON:def 8; :: thesis: verum