take REAL ; :: thesis: ( not REAL is countable & not REAL is empty )
thus ( not REAL is countable & not REAL is empty ) ; :: thesis: verum