theorem Th3: :: TOPDIM_2:3

for n being Nat
for X being set
for Fx being Subset-Family of X st ( for G being finite Subset-Family of X st G c= Fx & n + 1 < card G holds
meet G is empty ) holds
order Fx <= n