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