let p be Prime; :: thesis: card (FreeGen p) <= 2 |^ p
Segm (card (FreeGen p)) c= Segm (2 |^ p) by LmX;
hence card (FreeGen p) <= 2 |^ p by NAT_1:39; :: thesis: verum