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 Th44, XBOOLE_1:26;
then A2: (P `) /\ (Int P) c= {} TS by A1, XBOOLE_0:def 7;
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:52;
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 Th65
.= P \/ (((Int P) `) /\ P) by SUBSET_1:32
.= (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