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 object ; :: 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 and
B is finite and
A2: x = Intersect B by CANTOR_1:def 3;
B = {} by A1;
then x = X by A2, SETFAM_1:def 9;
hence x in {X} by TARSKI:def 1; :: thesis: verum
end;
let x be object ; :: 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 A3: x = X by TARSKI:def 1;
Intersect ({} (bool X)) = X by SETFAM_1:def 9;
hence x in FinMeetCl A by A3, CANTOR_1:def 3; :: thesis: verum