let T be TopSpace; :: thesis: Int (Cl ({} T)) = {} T
Int (Cl ({} T)) = Int ({} T) by PCOMPS_1:2
.= {} T ;
hence Int (Cl ({} T)) = {} T ; :: thesis: verum