let T be non empty TopSpace; for A being Subset of st T is T_1 holds
Der (Der A) c= Der A
let A be Subset of ; ( 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 set ; 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 x' = x as Point of ;
assume
not x in Der A
; contradiction
then consider G being open Subset of such that
A3:
x' in G
and
A4:
for y being Point of holds
( not y in A /\ G or not x' <> y )
by Th19;
Cl {x'} = {x'}
by A1, YELLOW_8:35;
then A5:
G \ {x'} is open
by FRECHET:4;
consider y being Point of such that
A6:
y in (Der A) /\ G
and
A7:
x <> y
by A2, A3, Th19;
y in Der A
by A6, XBOOLE_0:def 4;
then A8:
y in (Der A) \ {x}
by A7, ZFMISC_1:64;
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 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 \ {x'};
A12:
G misses A \ {x}
q in Der A
by A10, XBOOLE_0:def 5;
then consider y being Point of such that
A15:
y in A /\ (G \ {x'})
and
A16:
q <> y
by A11, A5, Th19;
y in A
by A15, XBOOLE_0:def 4;
then A17:
y in A \ {q}
by A16, ZFMISC_1:64;
y in G \ {x'}
by A15, XBOOLE_0:def 4;
then consider f being set such that
A18:
f in G \ {x'}
and
A19:
f in A \ {q}
by A17;
( f <> x' & f in A )
by A18, A19, ZFMISC_1:64;
then A20:
f in A \ {x'}
by ZFMISC_1:64;
f in G
by A18, ZFMISC_1:64;
hence
contradiction
by A12, A20, XBOOLE_0:3; verum