2,3,5,7,11 are_mutually_distinct by ZFMISC_1:def 7;
then 5 = card (SetPrimenumber 13) by LS13, CARD_2:63;
hence primenumber 5 = 13 by NAT_4:28, NEWTON:def 8; :: thesis: verum