take [#] REAL ; :: thesis: ( [#] REAL is open & [#] REAL is closed & [#] REAL is interval & not [#] REAL is empty & not [#] REAL is real-bounded )
thus ( [#] REAL is open & [#] REAL is closed & [#] REAL is interval & not [#] REAL is empty & not [#] REAL is real-bounded ) ; :: thesis: verum