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