:: deftheorem Def1 defines finite-order TOPDIM_2:def 1 :
for X being set
for Fx being Subset-Family of X holds
( Fx is finite-order iff ex n being Nat st
for Gx being Subset-Family of X st Gx c= Fx & n in card Gx holds
meet Gx is empty );