let TS be TopSpace; :: thesis: for K being Subset of TS holds Cl (Fr K) = Fr K
let K be Subset of TS; :: thesis: Cl (Fr K) = Fr K
A1: Cl (Cl (K `)) = Cl (K `) ;
Cl (Cl K) = Cl K ;
hence Cl (Fr K) = Fr K by A1, Th7; :: thesis: verum