let GX be TopStruct ; :: thesis: for R being Subset of GX st R is closed_condensed holds
Fr R c= Cl (Int R)
let R be Subset of GX; :: thesis: ( R is closed_condensed implies Fr R c= Cl (Int R) )
assume R is closed_condensed ; :: thesis: Fr R c= Cl (Int R)
then R = Cl (Int R) by Def7;
hence Fr R c= Cl (Int R) by XBOOLE_1:17; :: thesis: verum