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 & (N-min X) `2 = N-bound X & (N-max X) `2 = N-bound X & (NE-corner X) `2 = N-bound X ) by EUCLID:56;
( (NW-corner X) `1 <= (N-min X) `1 & (NW-corner X) `1 <= (N-max X) `1 & (N-min X) `1 <= (NE-corner X) `1 & (N-max X) `1 <= (NE-corner X) `1 ) by Th97;
then ( N-min X in LSeg (NW-corner X),(NE-corner X) & N-max X in LSeg (NW-corner X),(NE-corner X) ) by A1, GOBOARD7:9;
hence LSeg (N-min X),(N-max X) c= LSeg (NW-corner X),(NE-corner X) by TOPREAL1:12; :: thesis: verum