let GX be TopStruct ; :: thesis: for R being Subset of GX st R is open & R is closed holds
( R is closed_condensed iff R is open_condensed )
let R be Subset of GX; :: thesis: ( R is open & R is closed implies ( R is closed_condensed iff R is open_condensed ) )
assume that
A1: R is open and
A2: R is closed ; :: thesis: ( R is closed_condensed iff R is open_condensed )
thus ( R is closed_condensed iff R is open_condensed ) :: thesis: verum

proof

A3: R = Cl R by A2, PRE_TOPC:52;
R = Int R by A1, Th55;
hence ( R is closed_condensed iff R is open_condensed ) by A3, Def7, Def8; :: thesis: verum

end;