let C be non empty compact Subset of (TOP-REAL 2); :: thesis: N-min C in LSeg ((NW-corner C),(NE-corner C))
A1: N-most C c= LSeg ((NW-corner C),(NE-corner C)) by XBOOLE_1:17;
N-min C in N-most C by PSCOMP_1:42;
hence N-min C in LSeg ((NW-corner C),(NE-corner C)) by A1; :: thesis: verum