let T be non empty TopSpace; :: thesis: for A being Subset of T holds Der A c= Cl A
let A be Subset of T; :: thesis: Der A c= Cl A
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Der A or x in Cl A )
assume A1: x in Der A ; :: thesis: x in Cl A
then reconsider x9 = x as Point of T ;
for G being Subset of T st G is open & x9 in G holds
A meets G
proof
let G be Subset of T; :: thesis: ( G is open & x9 in G implies A meets G )
assume A2: G is open ; :: thesis: ( not x9 in G or A meets G )
assume x9 in G ; :: thesis: A meets G
then ex y being Point of T st
( y in A /\ G & x <> y ) by A1, A2, Th17;
hence A meets G ; :: thesis: verum
end;
hence x in Cl A by PRE_TOPC:24; :: thesis: verum