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 Th48, 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 Th44, PRE_TOPC:19;
hence Cl (Int T) = Cl (Int (Cl (Int T))) by A1, XBOOLE_0:def 10; :: thesis: verum