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 ) )
assume R is condensed ; :: thesis: ( Int R is condensed & Cl R is condensed )
then A1: ( Int (Cl R) c= R & R c= Cl (Int R) ) by Def6;
A2: R c= Cl R by PRE_TOPC:48;
then A3: Int (Cl (Cl R)) c= Cl R by A1, XBOOLE_1:1;
Int R c= R by Th44;
then A4: Int R c= Cl (Int (Int R)) by A1, XBOOLE_1:1;
(Cl R) ` c= R ` by A2, 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 A5: Cl (Int R) c= Cl ((Cl ((Cl R) ` )) ` ) by PRE_TOPC:49;
Cl R c= Cl (Cl (Int R)) by A1, PRE_TOPC:49;
then A6: Cl R c= Cl (Int (Cl R)) by A5, XBOOLE_1:1;
Cl (Int R) c= Cl R by Th44, PRE_TOPC:49;
then A7: Int (Cl (Int R)) c= Int (Cl R) by Th48;
Int (Int (Cl R)) c= Int R by A1, Th48;
then Int (Cl (Int R)) c= Int R by A7, XBOOLE_1:1;
hence ( Int R is condensed & Cl R is condensed ) by A3, A4, A6, Def6; :: thesis: verum