let TS be TopSpace; :: thesis: for GX being TopStruct
for P being Subset of TS
for R being Subset of GX holds
( ( R is open & R is condensed implies R is open_condensed ) & ( P is open_condensed implies ( P is open & P is condensed ) ) )
let GX be TopStruct ; :: thesis: for P being Subset of TS
for R being Subset of GX holds
( ( R is open & R is condensed implies R is open_condensed ) & ( P is open_condensed implies ( P is open & P is condensed ) ) )
let P be Subset of TS; :: thesis: for R being Subset of GX holds
( ( R is open & R is condensed implies R is open_condensed ) & ( P is open_condensed implies ( P is open & P is condensed ) ) )
let R be Subset of GX; :: thesis: ( ( R is open & R is condensed implies R is open_condensed ) & ( P is open_condensed implies ( P is open & P is condensed ) ) )
hereby :: thesis: ( P is open_condensed implies ( P is open & P is condensed ) )
assume that
A1: R is open and
A2: R is condensed ; :: thesis: R is open_condensed
R = Int R by A1, Th23;
then A3: R c= Int (Cl R) by Th19, PRE_TOPC:18;
Int (Cl R) c= R by A2;
then Int (Cl R) = R by A3;
hence R is open_condensed ; :: thesis: verum
end;
assume A4: P is open_condensed ; :: thesis: ( P is open & P is condensed )
then A5: Fr (Cl P) = (Cl P) \ P by Th64;
Fr P = Fr (Cl P) by A4;
then P is open by A5, Th42;
then Int P = P by Th23;
then A6: P c= Cl (Int P) by PRE_TOPC:18;
P = Int (Cl P) by A4;
hence ( P is open & P is condensed ) by A6; :: thesis: verum