take TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) ; :: thesis: ( TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) is strict & not TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) is empty & TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) is real-functions-membered )
thus ( TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) is strict & not TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) is empty & TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) is real-functions-membered ) ; :: thesis: verum