let X be set ; :: thesis: for A being Subset-Family of X st A = {{} ,X} holds
( UniCl A = A & FinMeetCl A = A )
let A be Subset-Family of X; :: thesis: ( A = {{} ,X} implies ( UniCl A = A & FinMeetCl A = A ) )
assume A1: A = {{} ,X} ; :: thesis: ( UniCl A = A & FinMeetCl A = A )

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: ( A c= UniCl A & FinMeetCl A = A )

let a be set ; :: thesis: ( a in UniCl A implies a in A )
assume a in UniCl A ; :: thesis: a in A
then consider y being Subset-Family of X such that
A2: ( y c= A & a = union y ) by CANTOR_1:def 1;
( y = {} or y = {{} } or y = {X} or y = {{} ,X} ) by A1, A2, ZFMISC_1:42;
then ( a = {} or a = X or ( a = {} \/ X & {} \/ X = X ) ) by A2, ZFMISC_1:2, ZFMISC_1:31, ZFMISC_1:93;
hence a in A by A1, TARSKI:def 2; :: thesis: verum

end;

thus A c= UniCl A by CANTOR_1:1; :: thesis: FinMeetCl A = A

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

let a be set ; :: thesis: ( a in FinMeetCl A implies a in A )
assume a in FinMeetCl A ; :: thesis: a in A
then consider y being Subset-Family of X such that
A3: ( y c= A & y is finite & a = Intersect y ) by CANTOR_1:def 4;
( y = {} or y = {{} } or y = {X} or y = {{} ,X} ) by A1, A3, ZFMISC_1:42;
then ( a = X or a = meet {{} } or a = meet {X} or a = meet {{} ,X} ) by A3, SETFAM_1:def 10;
then ( a = X or a = {} or ( a = {} /\ X & {} /\ X = {} ) ) by SETFAM_1:11, SETFAM_1:12;
hence a in A by A1, TARSKI:def 2; :: thesis: verum

end;

thus A c= FinMeetCl A by CANTOR_1:4; :: thesis: verum