let S, S9 be Subset of X; :: thesis:
assume that
A2: ex F being Subset-Family of X st
( ( for A being Subset of X holds
( A in F iff ( A is open & A is closed & x in A ) ) ) & meet F = S ) and
A3: ex F9 being Subset-Family of X st
( ( for A being Subset of X holds
( A in F9 iff ( A is open & A is closed & x in A ) ) ) & meet F9 = S9 ) ; :: thesis:
consider F being Subset-Family of X such that
A4: for A being Subset of X holds
( A in F iff ( A is open & A is closed & x in A ) ) and
A5: meet F = S by A2;
consider F9 being Subset-Family of X such that
A6: for A being Subset of X holds
( A in F9 iff ( A is open & A is closed & x in A ) ) and
A7: meet F9 = S9 by A3;
A8: F9 <> {} by A6, Th22;
A9: F <> {} by A4, Th22;

now :: thesis:

let y be object ; :: thesis:

A10: now :: thesis:

assume A11: y in S9 ; :: thesis:
for B being set st B in F holds
y in B

proof

let B be set ; :: thesis:
assume A12: B in F ; :: thesis:
then reconsider B1 = B as Subset of X ;
( B1 is open & B1 is closed & x in B1 ) by A4, A12;
then B1 in F9 by A6;
hence y in B by A7, A11, SETFAM_1:def 1; :: thesis:

end;

hence y in S by A5, A9, SETFAM_1:def 1; :: thesis:

end;

now :: thesis:

assume A13: y in S ; :: thesis:
for B being set st B in F9 holds
y in B

proof

let B be set ; :: thesis:
assume A14: B in F9 ; :: thesis:
then reconsider B1 = B as Subset of X ;
( B1 is open & B1 is closed & x in B1 ) by A6, A14;
then B1 in F by A4;
hence y in B by A5, A13, SETFAM_1:def 1; :: thesis:

end;

hence y in S9 by A7, A8, SETFAM_1:def 1; :: thesis:

end;

hence ( y in S iff y in S9 ) by A10; :: thesis:

end;

hence S = S9 by TARSKI:2; :: thesis: