let X be non empty compact Subset of (TOP-REAL 2); :: thesis: LSeg ((N-min X),(N-max X)) c= LSeg ((NW-corner X),(NE-corner X))
A1: ( (NW-corner X) `2 = N-bound X & (NE-corner X) `2 = N-bound X ) by EUCLID:52;
A2: (N-max X) `1 <= (NE-corner X) `1 by Th38;
( (N-max X) `2 = N-bound X & (NW-corner X) `1 <= (N-max X) `1 ) by Th38, EUCLID:52;
then A3: N-max X in LSeg ((NW-corner X),(NE-corner X)) by A1, A2, GOBOARD7:8;
A4: (N-min X) `1 <= (NE-corner X) `1 by Th38;
( (N-min X) `2 = N-bound X & (NW-corner X) `1 <= (N-min X) `1 ) by Th38, EUCLID:52;
then N-min X in LSeg ((NW-corner X),(NE-corner X)) by A1, A4, GOBOARD7:8;
hence LSeg ((N-min X),(N-max X)) c= LSeg ((NW-corner X),(NE-corner X)) by A3, TOPREAL1:6; :: thesis: verum