let TS be TopSpace; :: thesis: for P being Subset of TS holds
( P is open iff Fr P = (Cl P) \ P )
let P be Subset of TS; :: thesis: ( P is open iff Fr P = (Cl P) \ P )
A1: Fr P misses (Fr P) ` by XBOOLE_1:79;
A2: Int P c= P by Th44;

hereby :: thesis: ( Fr P = (Cl P) \ P implies P is open )

assume P is open ; :: thesis: Fr P = (Cl P) \ P
then P = Int P by Th55;
hence Fr P = (Cl P) \ P by Lm2; :: thesis: verum

end;

assume A3: Fr P = (Cl P) \ P ; :: thesis: P is open
(Cl P) \ (Fr P) = (P \/ (Fr P)) \ (Fr P) by Th65
.= ((Fr P) ` ) /\ (P \/ (Fr P)) by SUBSET_1:32
.= (P /\ ((Fr P) ` )) \/ (((Fr P) ` ) /\ (Fr P)) by XBOOLE_1:23
.= (P \ (Fr P)) \/ ((Fr P) /\ ((Fr P) ` )) by SUBSET_1:32
.= (Int P) \/ ((Fr P) /\ ((Fr P) ` )) by Th74
.= (Int P) \/ ({} TS) by A1, XBOOLE_0:def 7
.= Int P ;
then P c= Int P by A3, Lm5, PRE_TOPC:48;
hence P is open by A2, XBOOLE_0:def 10; :: thesis: verum