set Sq = R^2-unit_square ;
thus R^2-unit_square is special_polygonal by SPPOL_2:61; :: thesis: ( not R^2-unit_square is horizontal & not R^2-unit_square is vertical )
A1: (LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|) c= R^2-unit_square by XBOOLE_1:7;
A2: LSeg |[0 ,0 ]|,|[0 ,1]| c= (LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|) by XBOOLE_1:7;
( |[0 ,0 ]| `2 = 0 & |[0 ,1]| `2 = 1 ) by EUCLID:56;
then not LSeg |[0 ,0 ]|,|[0 ,1]| is horizontal by SPPOL_1:36;
hence not R^2-unit_square is horizontal by A1, A2, Th11, XBOOLE_1:1; :: thesis: not R^2-unit_square is vertical
A3: LSeg |[0 ,1]|,|[1,1]| c= (LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|) by XBOOLE_1:7;
( |[0 ,1]| `1 = 0 & |[1,1]| `1 = 1 ) by EUCLID:56;
then not LSeg |[0 ,1]|,|[1,1]| is vertical by SPPOL_1:37;
hence not R^2-unit_square is vertical by A1, A3, Th12, XBOOLE_1:1; :: thesis: verum