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) )
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 Lm4; :: thesis: verum

end;

assume A1: Fr P = P \ (Int P) ; :: thesis: P is closed
A2: P ` misses P by XBOOLE_1:79;
(P ` ) /\ (Int P) c= (P ` ) /\ P by Th44, XBOOLE_1:26;
then A3: (P ` ) /\ (Int P) c= {} TS by A2, XBOOLE_0:def 7;
A4: ((P ` ) ` ) \/ ((Int P) ` ) = ((P ` ) /\ (Int P)) ` by XBOOLE_1:54;
Cl P = P \/ (P \ (Int P)) by A1, Th65
.= P \/ (((Int P) ` ) /\ P) by SUBSET_1:32
.= (P \/ ((Int P) ` )) /\ (P \/ P) by XBOOLE_1:24
.= (({} TS) ` ) /\ P by A3, A4
.= P by XBOOLE_1:28 ;
hence P is closed ; :: thesis: verum