A1: R^2-unit_square = (((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[1,1]|,|[1,0 ]|)) \/ (LSeg |[1,0 ]|,|[0 ,0 ]|) by TOPREAL1:def 4, XBOOLE_1:4;
( LSeg |[0 ,0 ]|,|[0 ,1]| meets LSeg |[0 ,1]|,|[1,1]| & LSeg |[0 ,0 ]|,|[1,0 ]| meets LSeg |[1,0 ]|,|[1,1]| & LSeg |[0 ,1]|,|[1,1]| meets LSeg |[1,0 ]|,|[1,1]| ) by TOPREAL1:21, TOPREAL1:22, TOPREAL1:24, XBOOLE_0:def 7;
hence R^2-unit_square is connected by A1, JORDAN1:8; :: thesis: verum