let T be non empty TopSpace; :: thesis: for A being Subset of holds Der A c= Cl A
let A be Subset of ; :: thesis: Der A c= Cl A
let x be set ; :: 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 x' = x as Point of ;
for G being Subset of st G is open & x' in G holds
A meets G

proof

let G be Subset of ; :: thesis: ( G is open & x' in G implies A meets G )
assume A2: G is open ; :: thesis: ( not x' in G or A meets G )
assume x' in G ; :: thesis: A meets G
then ex y being Point of st
( y in A /\ G & x <> y ) by A1, A2, Th19;
hence A meets G by XBOOLE_0:4; :: thesis: verum

end;

hence x in Cl A by PRE_TOPC:54; :: thesis: verum