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 object ; :: 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 and
A3: a = union y by CANTOR_1:def 1;
( y = {} or y = {{}} or y = {X} or y = {{},X} ) by A1, A2, ZFMISC_1:36;
then ( a = {} or a = X or ( a = {} \/ X & {} \/ X = X ) ) by A3, ZFMISC_1:2, ZFMISC_1:25, ZFMISC_1:75;
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 object ; :: 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
A4: y c= A and
y is finite and
A5: a = Intersect y by CANTOR_1:def 3;
( y = {} or y = {{}} or y = {X} or y = {{},X} ) by A1, A4, ZFMISC_1:36;
then ( a = X or a = meet {{}} or a = meet {X} or a = meet {{},X} ) by A5, SETFAM_1:def 9;
then ( a = X or a = {} or ( a = {} /\ X & {} /\ X = {} ) ) by SETFAM_1:10, SETFAM_1:11;
hence a in A by A1, TARSKI:def 2; :: thesis: verum
end;
thus A c= FinMeetCl A by CANTOR_1:4; :: thesis: verum