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

now

let y be set ; :: thesis: ( y in S iff y in S' )

A10: now

assume A11: y in S' ; :: 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 ;
( B1 is open & B1 is closed & x in B1 ) by A4, A12;
then B1 in F' 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

assume A13: y in S ; :: 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 A14: B in F' ; :: thesis: y in B
then reconsider B1 = B as Subset of ;
( 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 S' by A7, A8, SETFAM_1:def 1; :: thesis: verum

end;

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

end;

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