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 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 T ;
for G being Subset of T st G is open & x' in G holds
A meets G

proof

let G be Subset of T; :: 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 consider y being Point of T such that
A3: ( y in A /\ G & x <> y ) by A1, A2, Th19;
thus A meets G by A3, XBOOLE_0:4; :: thesis: verum

end;

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