Formalization of Formal Topology by Means of the Interactive Theorem Prover Matita