let TS be TopSpace; :: thesis: for P being Subset of TS holds
( P is closed iff Fr P = P \ (Int P) )
let P be Subset of TS; :: thesis: ( P is closed iff Fr P = P \ (Int P) )
A1: P ` misses P by XBOOLE_1:79;
(P `) /\ (Int P) c= (P `) /\ P by Th16, XBOOLE_1:26;
then A2: (P `) /\ (Int P) c= {} TS by A1;
thus ( P is closed implies Fr P = P \ (Int P) ) :: thesis: ( Fr P = P \ (Int P) implies P is closed )

proof

assume P is closed ; :: thesis: Fr P = P \ (Int P)
then P = Cl P by PRE_TOPC:22;
hence Fr P = P \ (Int P) by Lm2; :: thesis: verum

end;

A3: ((P `) `) \/ ((Int P) `) = ((P `) /\ (Int P)) ` by XBOOLE_1:54;
assume Fr P = P \ (Int P) ; :: thesis: P is closed
then Cl P = P \/ (P \ (Int P)) by Th31
.= P \/ (((Int P) `) /\ P) by SUBSET_1:13
.= (P \/ ((Int P) `)) /\ (P \/ P) by XBOOLE_1:24
.= (({} TS) `) /\ P by A2, A3
.= P by XBOOLE_1:28 ;
hence P is closed ; :: thesis: verum