let GX be TopStruct ; :: thesis: for R being Subset of GX st R is condensed holds
( Int R is condensed & Cl R is condensed )
let R be Subset of GX; :: thesis: ( R is condensed implies ( Int R is condensed & Cl R is condensed ) )
Cl (Int R) c= Cl R by Th44, PRE_TOPC:49;
then A1: Int (Cl (Int R)) c= Int (Cl R) by Th48;
A2: R c= Cl R by PRE_TOPC:48;
then (Cl R) ` c= R ` by SUBSET_1:31;
then Cl ((Cl R) ` ) c= Cl (R ` ) by PRE_TOPC:49;
then (Cl (R ` )) ` c= (Cl ((Cl R) ` )) ` by SUBSET_1:31;
then A3: Cl (Int R) c= Cl ((Cl ((Cl R) ` )) ` ) by PRE_TOPC:49;
assume A4: R is condensed ; :: thesis: ( Int R is condensed & Cl R is condensed )
then A5: R c= Cl (Int R) by Def6;
then Cl R c= Cl (Cl (Int R)) by PRE_TOPC:49;
then A6: Cl R c= Cl (Int (Cl R)) by A3, XBOOLE_1:1;
A7: Int (Cl R) c= R by A4, Def6;
then Int (Int (Cl R)) c= Int R by Th48;
then A8: Int (Cl (Int R)) c= Int R by A1, XBOOLE_1:1;
Int R c= R by Th44;
then A9: Int R c= Cl (Int (Int R)) by A5, XBOOLE_1:1;
Int (Cl (Cl R)) c= Cl R by A7, A2, XBOOLE_1:1;
hence ( Int R is condensed & Cl R is condensed ) by A9, A6, A8, Def6; :: thesis: verum