let TS be TopSpace; :: thesis: for GX being TopStruct
for P being Subset of TS
for R being Subset of GX holds
( ( R is closed & R is condensed implies R is closed_condensed ) & ( P is closed_condensed implies ( P is closed & P is condensed ) ) )
let GX be TopStruct ; :: thesis: for P being Subset of TS
for R being Subset of GX holds
( ( R is closed & R is condensed implies R is closed_condensed ) & ( P is closed_condensed implies ( P is closed & P is condensed ) ) )
let P be Subset of TS; :: thesis: for R being Subset of GX holds
( ( R is closed & R is condensed implies R is closed_condensed ) & ( P is closed_condensed implies ( P is closed & P is condensed ) ) )
let R be Subset of GX; :: thesis: ( ( R is closed & R is condensed implies R is closed_condensed ) & ( P is closed_condensed implies ( P is closed & P is condensed ) ) )

hereby :: thesis: ( P is closed_condensed implies ( P is closed & P is condensed ) )

assume that
A1: R is closed and
A2: R is condensed ; :: thesis: R is closed_condensed
A3: R = Cl R by A1, PRE_TOPC:22;
then Int R c= R by A2;
then A4: Cl (Int R) c= R by A3, PRE_TOPC:19;
R c= Cl (Int R) by A2;
then Cl (Int R) = R by A4;
hence R is closed_condensed ; :: thesis: verum

end;

assume A5: P is closed_condensed ; :: thesis: ( P is closed & P is condensed )
Fr (Int P) = (Cl (Int P)) \ (Int (Int P)) by Lm2;
then Fr P = (Cl (Int P)) \ (Int (Int P)) by A5
.= P \ (Int P) by A5 ;
then P is closed by Th43;
then Cl P = P by PRE_TOPC:22;
then A6: Int (Cl P) c= P by Th16;
Cl (Int P) = P by A5;
hence ( P is closed & P is condensed ) by A6; :: thesis: verum