set X = R^2-unit_square ;
( (LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|) c= R^2-unit_square & LSeg |[0 ,1]|,|[1,1]| c= (LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|) ) by XBOOLE_1:7;
hence N-most R^2-unit_square = LSeg |[0 ,1]|,|[1,1]| by Th35, Th36, Th37, XBOOLE_1:1, XBOOLE_1:28; :: thesis: verum