let p be Prime; :: thesis: card (FreeGen p) c= card (BoolePrime p)
A1: dom (canHom p) = FreeGen p by FUNCT_2:def 1;
rng (canHom p) c= BoolePrime p by RELAT_1:def 19;
hence card (FreeGen p) c= card (BoolePrime p) by A1, CARD_1:10; :: thesis: verum