2 = card (SetPrimenumber 5) by LS3, CARD_2:57;
hence primenumber 2 = 5 by PEPIN:59, NEWTON:def 8; :: thesis: verum