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)

thus Cl A c= A \/ (Der A) :: according to XBOOLE_0:def 10 :: thesis: A \/ (Der A) c= Cl A

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Cl A or x in A \/ (Der A) )
assume A2: x in Cl A ; :: thesis: x in A \/ (Der A)
then reconsider x' = 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 A3: not x in A ; :: thesis: x in A \/ (Der A)

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

proof

let U be open Subset of T; :: thesis: ( x' in U implies ex y being Point of T st
( y in A /\ U & x' <> y ) )
assume x' in U ; :: thesis: ex y being Point of T st
( y in A /\ U & x' <> y )
then A meets U by A2, PRE_TOPC:54;
then consider y being set such that
A4: ( y in A & y in U ) by XBOOLE_0:3;
reconsider y = y as Point of T by A4;
take y ; :: thesis: ( y in A /\ U & x' <> y )
thus ( y in A /\ U & x' <> y ) by A3, A4, XBOOLE_0:def 4; :: thesis: verum

end;

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

end;

end;

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A \/ (Der A) or x in Cl A )
assume A5: x in A \/ (Der A) ; :: thesis: x in Cl A
A6: Der A c= Cl A by A1, Th30;

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

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

A c= Cl A by PRE_TOPC:48;
hence x in Cl A by A7; :: thesis: verum

end;

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

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

end;

end;

end;

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

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

end;

end;