for GX being TopStruct
for R being Subset of GX st R is open & R is closed holds
( R is closed_condensed iff R is open_condensed ) by PRE_TOPC:22, Th23;