let T be non empty TopSpace; :: thesis: for A being Subset of T st T is T_1 holds
Der (Der A) c= Der A
let A be Subset of T; :: thesis: ( T is T_1 implies Der (Der A) c= Der A )
assume A1: T is T_1 ; :: thesis: Der (Der A) c= Der A
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Der (Der A) or x in Der A )
assume A2: x in Der (Der A) ; :: thesis: x in Der A
then reconsider x' = x as Point of T ;
assume not x in Der A ; :: thesis: contradiction
then consider G being open Subset of T such that
A3: ( x' in G & ( for y being Point of T holds
( not y in A /\ G or not x' <> y ) ) ) by Th19;
consider y being Point of T such that
A4: ( y in (Der A) /\ G & x <> y ) by A2, A3, Th19;
A5: ( y in Der A & y in G ) by A4, XBOOLE_0:def 4;
then A6: y in (Der A) \ {x} by A4, ZFMISC_1:64;
A7: G misses A \ {x}

proof

assume G meets A \ {x} ; :: thesis: contradiction
then consider g being set such that
A8: ( g in G & g in A \ {x} ) by XBOOLE_0:3;
g in A by A8, XBOOLE_0:def 5;
then g in A /\ G by A8, XBOOLE_0:def 4;
then x' = g by A3;
hence contradiction by A8, ZFMISC_1:64; :: thesis: verum

end;

consider q being set such that
A9: ( q in G & q in (Der A) \ {x} ) by A5, A6;
reconsider q = q as Point of T by A9;
A10: not q in {x} by A9, XBOOLE_0:def 5;
A11: q in Der A by A9, XBOOLE_0:def 5;
A12: q in G \ {x} by A9, A10, XBOOLE_0:def 5;
Cl {x'} = {x'} by A1, YELLOW_8:35;
then A13: G \ {x'} is open by FRECHET:4;
set U = G \ {x'};
consider y being Point of T such that
A14: ( y in A /\ (G \ {x'}) & q <> y ) by A11, A12, A13, Th19;
A15: ( y in A & y in G \ {x'} ) by A14, XBOOLE_0:def 4;
then y in A \ {q} by A14, ZFMISC_1:64;
then consider f being set such that
A16: ( f in G \ {x'} & f in A \ {q} ) by A15;
A17: ( f in G & f <> x' ) by A16, ZFMISC_1:64;
f in A by A16, ZFMISC_1:64;
then f in A \ {x'} by A17, ZFMISC_1:64;
hence contradiction by A7, A17, XBOOLE_0:3; :: thesis: verum