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