reconsider E = {} as Subset-Family of X by XBOOLE_1:2;

take E ; :: thesis: E is finite-order

take 0 ; :: according to TOPDIM_2:def 1 :: thesis: for Gx being Subset-Family of X st Gx c= E & 0 in card Gx holds

meet Gx is empty

let G be Subset-Family of X; :: thesis: ( G c= E & 0 in card G implies meet G is empty )

thus ( G c= E & 0 in card G implies meet G is empty ) ; :: thesis: verum

take E ; :: thesis: E is finite-order

take 0 ; :: according to TOPDIM_2:def 1 :: thesis: for Gx being Subset-Family of X st Gx c= E & 0 in card Gx holds

meet Gx is empty

let G be Subset-Family of X; :: thesis: ( G c= E & 0 in card G implies meet G is empty )

thus ( G c= E & 0 in card G implies meet G is empty ) ; :: thesis: verum