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

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