let GX be TopStruct ; :: thesis: for R being Subset of GX st R is open_condensed holds
( Fr R = Fr (Cl R) & Fr (Cl R) = (Cl R) \ R )
let R be Subset of GX; :: thesis: ( R is open_condensed implies ( Fr R = Fr (Cl R) & Fr (Cl R) = (Cl R) \ R ) )
assume R is open_condensed ; :: thesis: ( Fr R = Fr (Cl R) & Fr (Cl R) = (Cl R) \ R )
then R = Int (Cl R) by Def8;
hence ( Fr R = Fr (Cl R) & Fr (Cl R) = (Cl R) \ R ) by Lm2; :: thesis: verum