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 ) by SPPOL_2:63; :: thesis: verum