let T be non empty TopSpace; :: thesis: for A being Subset of T
for x being Point of T holds
( x in Der A iff for B being Basis of
for U being Subset of T st U in B holds
ex y being Point of T st
( y in A /\ U & x <> y ) )
let A be Subset of T; :: thesis: for x being Point of T holds
( x in Der A iff for B being Basis of
for U being Subset of T st U in B holds
ex y being Point of T st
( y in A /\ U & x <> y ) )
let x be Point of T; :: thesis: ( x in Der A iff for B being Basis of
for U being Subset of T st U in B holds
ex y being Point of T st
( y in A /\ U & x <> y ) )
hereby :: thesis: ( ( for B being Basis of
for U being Subset of T st U in B holds
ex y being Point of T st
( y in A /\ U & x <> y ) ) implies x in Der A )
assume x in Der A ; :: thesis: for B being Basis of
for U being Subset of T st U in B holds
ex y being Point of T st
( y in A /\ U & x <> y )
then x is_an_accumulation_point_of A by Th16;
then A1: x in Cl (A \ {x}) ;
let B be Basis of ; :: thesis: for U being Subset of T st U in B holds
ex y being Point of T st
( y in A /\ U & x <> y )
let U be Subset of T; :: thesis: ( U in B implies ex y being Point of T st
( y in A /\ U & x <> y ) )
assume U in B ; :: thesis: ex y being Point of T st
( y in A /\ U & x <> y )
then ( U is open & x in U ) by YELLOW_8:12;
then A \ {x} meets U by A1, PRE_TOPC:24;
then consider y being object such that
A2: y in A \ {x} and
A3: y in U by XBOOLE_0:3;
reconsider y = y as Point of T by A2;
take y = y; :: thesis: ( y in A /\ U & x <> y )
y in A by A2, ZFMISC_1:56;
hence ( y in A /\ U & x <> y ) by A2, A3, XBOOLE_0:def 4, ZFMISC_1:56; :: thesis: verum
end;
assume A4: for B being Basis of
for U being Subset of T st U in B holds
ex y being Point of T st
( y in A /\ U & x <> y ) ; :: thesis: x in Der A
for G being Subset of T st G is open & x in G holds
A \ {x} meets G
proof
set B = the Basis of ;
let G be Subset of T; :: thesis: ( G is open & x in G implies A \ {x} meets G )
assume A5: G is open ; :: thesis: ( not x in G or A \ {x} meets G )
assume x in G ; :: thesis: A \ {x} meets G
then consider V being Subset of T such that
A6: ( V in the Basis of & V c= G ) by A5, YELLOW_8:13;
( ex y being Point of T st
( y in A /\ V & x <> y ) & A /\ V c= A /\ G ) by A4, A6, XBOOLE_1:26;
then consider y being Point of T such that
A7: y in A /\ G and
A8: x <> y ;
y in A by A7, XBOOLE_0:def 4;
then A9: y in A \ {x} by A8, ZFMISC_1:56;
y in G by A7, XBOOLE_0:def 4;
hence A \ {x} meets G by A9, XBOOLE_0:3; :: thesis: verum
end;
then x in Cl (A \ {x}) by PRE_TOPC:24;
then x is_an_accumulation_point_of A ;
hence x in Der A by Th16; :: thesis: verum