take R^2-unit_square ; :: thesis: ( R^2-unit_square is being_simple_closed_curve & not R^2-unit_square is empty )
thus ( R^2-unit_square is being_simple_closed_curve & not R^2-unit_square is empty ) ; :: thesis: verum