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-min C in N-most C by PSCOMP_1:101;
N-most C c= LSeg (NW-corner C),(NE-corner C) by XBOOLE_1:17;
hence N-min C in LSeg (NW-corner C),(NE-corner C) by A1; :: thesis: verum