let X, Z be set ; :: thesis: for A being Subset-Family of X st A = {Z} holds
( FinMeetCl A = {Z,X} & UniCl A = {Z,{} } )
let A be Subset-Family of X; :: thesis: ( A = {Z} implies ( FinMeetCl A = {Z,X} & UniCl A = {Z,{} } ) )
assume A1: A = {Z} ; :: thesis: ( FinMeetCl A = {Z,X} & UniCl A = {Z,{} } )
thus FinMeetCl A c= {Z,X} :: according to XBOOLE_0:def 10 :: thesis: ( {Z,X} c= FinMeetCl A & UniCl A = {Z,{} } )

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in FinMeetCl A or x in {Z,X} )
assume x in FinMeetCl A ; :: thesis: x in {Z,X}
then consider Y being Subset-Family of X such that
A2: ( Y c= A & Y is finite & x = Intersect Y ) by CANTOR_1:def 4;
( Y = {} or Y = {Z} ) by A1, A2, ZFMISC_1:39;
then ( x = X or x = meet {Z} ) by A2, SETFAM_1:def 10;
then ( x = X or x = Z ) by SETFAM_1:11;
hence x in {Z,X} by TARSKI:def 2; :: thesis: verum

end;

reconsider E = {} as Subset-Family of X by XBOOLE_1:2;
reconsider E = E as Subset-Family of X ;

hereby :: according to TARSKI:def 3 :: thesis: UniCl A = {Z,{} }

let x be set ; :: thesis: ( x in {Z,X} implies x in FinMeetCl A )
assume x in {Z,X} ; :: thesis: x in FinMeetCl A
then ( x = X or x = Z ) by TARSKI:def 2;
then ( x = X or x = meet {Z} ) by SETFAM_1:11;
then ( ( x = Intersect E & E c= A ) or ( x = Intersect A & A c= A ) ) by A1, SETFAM_1:def 10, XBOOLE_1:2;
hence x in FinMeetCl A by A1, CANTOR_1:def 4; :: thesis: verum

end;

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

let x be set ; :: thesis: ( x in UniCl A implies x in {Z,{} } )
assume x in UniCl A ; :: thesis: x in {Z,{} }
then consider Y being Subset-Family of X such that
A3: ( Y c= A & x = union Y ) by CANTOR_1:def 1;
( Y = {} or Y = {Z} ) by A1, A3, ZFMISC_1:39;
then ( x = {} or x = Z ) by A3, ZFMISC_1:2, ZFMISC_1:31;
hence x in {Z,{} } by TARSKI:def 2; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {Z,{} } or x in UniCl A )
assume x in {Z,{} } ; :: thesis: x in UniCl A
then ( x = {} or x = Z ) by TARSKI:def 2;
then ( ( x = union E & E c= A ) or ( x = union A & A c= A ) ) by A1, XBOOLE_1:2, ZFMISC_1:2, ZFMISC_1:31;
hence x in UniCl A by CANTOR_1:def 1; :: thesis: verum