let T be non empty TopSpace; for A being Subset of T st T is T_1 holds
Der (Der A) c= Der A
let A be Subset of T; ( T is T_1 implies Der (Der A) c= Der A )
assume A1:
T is T_1
; Der (Der A) c= Der A
let x be object ; TARSKI:def 3 ( not x in Der (Der A) or x in Der A )
assume A2:
x in Der (Der A)
; x in Der A
then reconsider x9 = x as Point of T ;
assume
not x in Der A
; contradiction
then consider G being open Subset of T such that
A3:
x9 in G
and
A4:
for y being Point of T holds
( not y in A /\ G or not x9 <> y )
by Th17;
Cl {x9} = {x9}
by A1, YELLOW_8:26;
then A5:
G \ {x9} is open
by FRECHET:4;
consider y being Point of T such that
A6:
y in (Der A) /\ G
and
A7:
x <> y
by A2, A3, Th17;
y in Der A
by A6, XBOOLE_0:def 4;
then A8:
y in (Der A) \ {x}
by A7, ZFMISC_1:56;
y in G
by A6, XBOOLE_0:def 4;
then consider q being set such that
A9:
q in G
and
A10:
q in (Der A) \ {x}
by A8;
reconsider q = q as Point of T by A9;
not q in {x}
by A10, XBOOLE_0:def 5;
then A11:
q in G \ {x}
by A9, XBOOLE_0:def 5;
set U = G \ {x9};
A12:
G misses A \ {x}
q in Der A
by A10, XBOOLE_0:def 5;
then consider y being Point of T such that
A15:
y in A /\ (G \ {x9})
and
A16:
q <> y
by A11, A5, Th17;
y in A
by A15, XBOOLE_0:def 4;
then A17:
y in A \ {q}
by A16, ZFMISC_1:56;
y in G \ {x9}
by A15, XBOOLE_0:def 4;
then consider f being set such that
A18:
f in G \ {x9}
and
A19:
f in A \ {q}
by A17;
( f <> x9 & f in A )
by A18, A19, ZFMISC_1:56;
then A20:
f in A \ {x9}
by ZFMISC_1:56;
f in G
by A18, ZFMISC_1:56;
hence
contradiction
by A12, A20, XBOOLE_0:3; verum