take [#] REAL ; :: thesis: ( not [#] REAL is empty & [#] REAL is interval )
thus ( not [#] REAL is empty & [#] REAL is interval ) ; :: thesis: verum