theorem :: TOPS_1:63

for GX being TopStruct
for R being Subset of GX st R is closed_condensed holds
Fr R c= Cl (Int R) by XBOOLE_1:17;