2,3,5,7,11 are_mutually_distinct ;
hence card (primeNumbers (1,10)) = 5 by Th70, CARD_2:63; :: thesis: verum