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