take the topology of X ; :: thesis: ( the topology of X is open & the topology of X is quasi_basis )
thus ( the topology of X is open & the topology of X is quasi_basis ) ; :: thesis: verum