let GX be TopStruct ; :: thesis: for R being Subset of GX st R is open holds
Cl (Int (Cl R)) = Cl R
let R be Subset of GX; :: thesis: ( R is open implies Cl (Int (Cl R)) = Cl R )
assume A1: R is open ; :: thesis: Cl (Int (Cl R)) = Cl R
then Cl (Int (Cl R)) = Cl (Int (Cl (Int R))) by Th23
.= Cl (Int R) by Th26
.= Cl R by A1, Th23 ;
hence Cl (Int (Cl R)) = Cl R ; :: thesis: verum