Finite subfamilies retain the finite-generation obstruction

This is the finite-generation check of XXII-A and XXII-B, with its argument included here CheungXXIIA CheungXXIIB (prop:finite-generation). The auxiliary inner product is only a proof device.

The countable family in Definition def:class removes this particular finiteness premise. Proposition prop:empty-query shows why that removal alone is not a solution.