let F be Subset-Family of X; :: thesis: ( F is finite implies F is finite-order )
assume F is finite ; :: thesis: F is finite-order
then reconsider f = F as finite Subset-Family of X ;
take n = card f; :: according to TOPDIM_2:def 1 :: thesis: for Gx being Subset-Family of X st Gx c= F & n in card Gx holds
meet Gx is empty
let G be Subset-Family of X; :: thesis: ( G c= F & n in card G implies meet G is empty )
assume that
A1: G c= F and
A2: n in card G ; :: thesis: meet G is empty
card G c= Segm (card f) by A1, CARD_1:11;
hence meet G is empty by A2, NAT_1:44; :: thesis: verum