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 Th16, PRE_TOPC:19;
then A1: Int (Cl (Int R)) c= Int (Cl R) by Th19;
A2: R c= Cl R by PRE_TOPC:18;
then (Cl R) ` c= R ` by SUBSET_1:12;
then Cl ((Cl R) `) c= Cl (R `) by PRE_TOPC:19;
then (Cl (R `)) ` c= (Cl ((Cl R) `)) ` by SUBSET_1:12;
then A3: Cl (Int R) c= Cl ((Cl ((Cl R) `)) `) by PRE_TOPC:19;
assume A4: R is condensed ; :: thesis: ( Int R is condensed & Cl R is condensed )
then A5: R c= Cl (Int R) ;
then Cl R c= Cl (Cl (Int R)) by PRE_TOPC:19;
then A6: Cl R c= Cl (Int (Cl R)) by A3;
A7: Int (Cl R) c= R by A4;
then Int (Int (Cl R)) c= Int R by Th19;
then A8: Int (Cl (Int R)) c= Int R by A1;
Int R c= R by Th16;
then A9: Int R c= Cl (Int (Int R)) by A5;
Int (Cl (Cl R)) c= Cl R by A7, A2;
hence ( Int R is condensed & Cl R is condensed ) by A9, A6, A8; :: thesis: verum