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