A1: |[0,1]| `2 = 1 by EUCLID:52;
|[0,0]| `2 = 0 by EUCLID:52;
then A2: not LSeg (|[0,0]|,|[0,1]|) is horizontal by A1, SPPOL_1:15;
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, Th9, XBOOLE_1:1; :: thesis: not R^2-unit_square is vertical
A4: |[1,1]| `1 = 1 by EUCLID:52;
|[0,1]| `1 = 0 by EUCLID:52;
then A5: not LSeg (|[0,1]|,|[1,1]|) is vertical by A4, SPPOL_1:16;
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, Th10, XBOOLE_1:1; :: thesis: verum