for n being Nat
for X being set
for Fx being Subset-Family of X st order Fx <= n holds
Fx is finite-order