let GX be TopStruct ; :: thesis: for R being Subset of GX holds
( R is open_condensed iff R ` is closed_condensed )
let R be Subset of GX; :: thesis: ( R is open_condensed iff R ` is closed_condensed )
( R is open_condensed iff R = Int (Cl R) ) by Def8;
then ( R is open_condensed iff R ` = Cl (Int (R `)) ) ;
hence ( R is open_condensed iff R ` is closed_condensed ) by Def7; :: thesis: verum