let GX be TopStruct ; :: thesis: for T being Subset of GX holds Cl (Int T) = Cl (Int (Cl (Int T)))
let T be Subset of GX; :: thesis: Cl (Int T) = Cl (Int (Cl (Int T)))
Int (Int T) c= Int (Cl (Int T)) by Th19, PRE_TOPC:18;
then A1: Cl (Int T) c= Cl (Int (Cl (Int T))) by PRE_TOPC:19;
Cl (Int (Cl (Int T))) c= Cl (Cl (Int T)) by Th16, PRE_TOPC:19;
hence Cl (Int T) = Cl (Int (Cl (Int T))) by A1; :: thesis: verum