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