namespace http://mathhub.info/MitM/core/topology ❚
import base http://mathhub.info/MitM/Foundation ❚
import calc http://mathhub.info/MitM/core/calculus ❚

theory RealTopology : base:?Logic =
	include ☞calc:?RealMetricSpace❙
	include ☞calc:?MetricSpaceAsTopology ❙
	include ?OpenSetTopology ❙
	

	realTopology = metricAsTopology realmetricspace ❘ : topology ℝ❙
	realTopologicalSpace = [' universe := ℝ , topology := realTopology  '] ❘: topologicalSpace ❙
❚