let S, S9 be Subset of X; :: thesis: ( 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 ) & 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 = S9 ) implies S = S9 )
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: S = S9
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: for y being object holds
( y in S iff y in S9 )

let y be object ; :: thesis: ( y in S iff y in S9 )

A10: now :: thesis: ( y in S9 implies y in S )

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

proof

let B be set ; :: thesis: ( B in F implies y in B )
assume A12: B in F ; :: thesis: y in B
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: verum

end;

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

end;

now :: thesis: ( y in S implies y in S9 )

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

proof

let B be set ; :: thesis: ( B in F9 implies y in B )
assume A14: B in F9 ; :: thesis: y in B
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: verum

end;

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

end;

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

end;

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