Los sistemas de información geográfica han experimentado un crecimiento rápido durante décadas. La topología ha proporcionado valiosas herramientas de modelado en el desarrollo de este campo. La verificación formal del modelo de relaciones espaciales topológicas puede proporcionar una garantía fiable para la corrección de los sistemas de información geográfica. Presentamos una prueba del modelo de relaciones espaciales topológicas que ha sido formalmente verificada en el asistente de prueba Coq. Después de una introducción a la formalización de la teoría de conjuntos axiomática de Morse-Kelley, se desarrolla la descripción formal de los conceptos elementales y propiedades de la topología general. Las relaciones espaciales topológicas entre dos conjuntos se describen utilizando el concepto del valor de intersección. Finalmente, demostramos formalmente las relaciones espaciales topológicas entre dos conjuntos que están restringidas a las regiones espaciales regularmente cerradas y planas. Todos los detalles de la prueba se completan estrictamente en Coq, lo que muestra que la corrección del modelo teórico para los sistemas de información geográfica puede ser verificada por una computadora. Este documento proporciona un método novedoso para verificar la corrección del modelo de relaciones espaciales topológicas. Este trabajo también puede contribuir a la creación y validación de varios modelos y software geológicos.