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 object ; :: 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 and
Y is finite and
A3: x = Intersect Y by CANTOR_1:def 3;
( Y = {} or Y = {Z} ) by A1, A2, ZFMISC_1:33;
then ( x = X or x = meet {Z} ) by A3, SETFAM_1:def 9;
then ( x = X or x = Z ) by SETFAM_1:10;
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 object ; :: 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:10;
then ( ( x = Intersect E & E c= A ) or ( x = Intersect A & A c= A ) ) by A1, SETFAM_1:def 9;
hence x in FinMeetCl A by A1, CANTOR_1:def 3; :: thesis: verum

end;

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

let x be object ; :: 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
A4: Y c= A and
A5: x = union Y by CANTOR_1:def 1;
( Y = {} or Y = {Z} ) by A1, A4, ZFMISC_1:33;
then ( x = {} or x = Z ) by A5, ZFMISC_1:2, ZFMISC_1:25;
hence x in {Z,{}} by TARSKI:def 2; :: thesis: verum

end;

let x be object ; :: 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, ZFMISC_1:2, ZFMISC_1:25;
hence x in UniCl A by CANTOR_1:def 1; :: thesis: verum