4 = card (SetPrimenumber 11) by CARD_2:59, LS11;
hence primenumber 4 = 11 by NAT_4:27, NEWTON:def 8; :: thesis: verum