take the topology of X ; :: thesis: the topology of X is open
thus the topology of X is open ; :: thesis: verum