let X be set ; :: thesis: for A being Subset-Family of X holds X in FinMeetCl A
let A be Subset-Family of X; :: thesis: X in FinMeetCl A
{} is Subset-Family of X by XBOOLE_1:2;
then consider y being Subset-Family of X such that
A1: y = {} ;
( y c= A & Intersect y = X ) by A1, SETFAM_1:def 9;
hence X in FinMeetCl A by A1, Def3; :: thesis: verum