for GX being TopStruct
for R being Subset of GX holds
( R is open_condensed iff R ` is closed_condensed ) ;