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 Th31, Th32, Th33, XBOOLE_1:1, XBOOLE_1:28; :: thesis: verum