let T be TopSpace; :: thesis: for A being Subset of T holds Cl A = A \/ (Der A)
let A be Subset of T; :: thesis: Cl A = A \/ (Der A)

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

suppose A1: not T is empty ; :: thesis: Cl A = A \/ (Der A)

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Cl A or x in A \/ (Der A) )
assume A3: x in Cl A ; :: thesis: x in A \/ (Der A)
then reconsider x9 = x as Point of T ;

per cases ( x in A or not x in A ) ;

suppose x in A ; :: thesis: x in A \/ (Der A)

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

end;

suppose A4: not x in A ; :: thesis: x in A \/ (Der A)

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: ( x9 in U implies ex y being Point of T st
( y in A /\ U & x9 <> y ) )
assume x9 in U ; :: thesis: ex y being Point of T st
( y in A /\ U & x9 <> y )
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: ( y in A /\ U & x9 <> y )
thus ( y in A /\ U & x9 <> y ) by A4, A5, A6, XBOOLE_0:def 4; :: thesis: verum

end;

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

end;

end;

end;

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

per cases ( x in A or x in Der A ) by A7, XBOOLE_0:def 3;

suppose A8: x in A ; :: thesis: x in Cl A

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

end;

suppose x in Der A ; :: thesis: x in Cl A

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

end;

end;

end;

suppose A9: T is empty ; :: thesis: Cl A = A \/ (Der A)

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

end;

end;