take R^1 ; :: thesis: ( R^1 is connected & not R^1 is empty )
thus ( R^1 is connected & not R^1 is empty ) ; :: thesis: verum