theorem Th1: :: TOPDIM_2:1

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