let T be TopSpace; :: thesis:
let A be Subset of T; :: thesis:

per cases ;

suppose A1: not T is empty ; :: thesis:

then A2: Der A c= Cl A by Th28;
thus Cl A c= A \/ (Der A) :: according to XBOOLE_0:def 10 :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A3: x in Cl A ; :: thesis:
then reconsider x9 = x as Point of T ;

per cases ;

suppose x in A ; :: thesis:

hence x in A \/ (Der A) by XBOOLE_0:def 3; :: thesis:

end;

suppose A4: not x in A ; :: thesis:

for U being open Subset of T st x9 in U holds
ex y being Point of T st
( y in A /\ U & x9 <> y )

proof

let U be open Subset of T; :: thesis:
assume x9 in U ; :: thesis:
then A meets U by A3, PRE_TOPC:24;
then consider y being object such that
A5: y in A and
A6: y in U by XBOOLE_0:3;
reconsider y = y as Point of T by A5;
take y ; :: thesis:
thus ( y in A /\ U & x9 <> y ) by A4, A5, A6, XBOOLE_0:def 4; :: thesis:

end;

then x9 in Der A by A1, Th17;
hence x in A \/ (Der A) by XBOOLE_0:def 3; :: thesis:

end;

end;

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A7: x in A \/ (Der A) ; :: thesis:

per cases by A7, XBOOLE_0:def 3;

suppose A8: x in A ; :: thesis:

A c= Cl A by PRE_TOPC:18;
hence x in Cl A by A8; :: thesis:

end;

suppose x in Der A ; :: thesis:

hence x in Cl A by A2; :: thesis:

end;

end;

end;

suppose A9: T is empty ; :: thesis:

then the carrier of T is empty ;
then Cl A = {} \/ {}
.= A \/ (Der A) by A9 ;
hence Cl A = A \/ (Der A) ; :: thesis:

end;

end;