for GX being TopStruct
for R being Subset of GX st R is open_condensed holds
( Fr R = Fr (Cl R) & Fr (Cl R) = (Cl R) \ R ) by Lm2;