let T be TopSpace; :: thesis: for A being Subset of T st T is T_1 holds
Cl (Der A) = Der A
let A be Subset of T; :: thesis: ( T is T_1 implies Cl (Der A) = Der A )
assume A1: T is T_1 ; :: thesis: Cl (Der A) = Der A

per cases ( not T is empty or T is empty ) ;

suppose A2: not T is empty ; :: thesis: Cl (Der A) = Der A

Cl (Der A) = (Der A) \/ (Der (Der A)) by Th29;
then A3: Cl (Der A) c= (Der A) \/ (Der A) by A1, A2, Th32, XBOOLE_1:9;
Der A c= Cl (Der A) by PRE_TOPC:18;
hence Cl (Der A) = Der A by A3; :: thesis: verum

end;

suppose A4: T is empty ; :: thesis: Cl (Der A) = Der A

then Cl (Der A) = {} ;
hence Cl (Der A) = Der A by A4; :: thesis: verum

end;

end;