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 ;
A9: F <> {} by ;
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 ;
then B1 in F9 by A6;
hence y in B by ; :: thesis: verum
end;
hence y in S by ; :: 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 ;
then B1 in F by A4;
hence y in B by ; :: thesis: verum
end;
hence y in S9 by ; :: thesis: verum
end;
hence ( y in S iff y in S9 ) by A10; :: thesis: verum
end;
hence S = S9 by TARSKI:2; :: thesis: verum