let X be set ; :: thesis: for A being empty Subset-Family of X holds FinMeetCl A = {X}
let A be empty Subset-Family of X; :: thesis: FinMeetCl A = {X}

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {X} c= FinMeetCl A

let x be set ; :: thesis: ( x in FinMeetCl A implies x in {X} )
assume x in FinMeetCl A ; :: thesis: x in {X}
then consider B being Subset-Family of X such that
A1: ( B c= A & B is finite & x = Intersect B ) by CANTOR_1:def 4;
B = {} by A1;
then x = X by A1, SETFAM_1:def 10;
hence x in {X} by TARSKI:def 1; :: thesis: verum

end;

consider B being empty Subset-Family of X;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {X} or x in FinMeetCl A )
assume x in {X} ; :: thesis: x in FinMeetCl A
then ( x = X & B c= A & Intersect B = X ) by SETFAM_1:def 10, TARSKI:def 1;
hence x in FinMeetCl A by CANTOR_1:def 4; :: thesis: verum