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;

( ( 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 )

hence
S = S9
by TARSKI:2; :: thesis: verum( y in S iff y in S9 )

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

end;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

end;for B being set st B in F holds

y in B

proof

hence
y in S
by A5, A9, SETFAM_1:def 1; :: thesis: verum
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;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

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

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

for B being set st B in F9 holds

y in B

end;for B being set st B in F9 holds

y in B

proof

hence
y in S9
by A7, A8, SETFAM_1:def 1; :: thesis: verum
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;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