let X be non empty compact Subset of (TOP-REAL 2); :: thesis: LSeg (W-min X),(W-max X) c= LSeg (SW-corner X),(NW-corner X)
A1: ( (SW-corner X) `1 = W-bound X & (W-min X) `1 = W-bound X & (W-max X) `1 = W-bound X & (NW-corner X) `1 = W-bound X ) by EUCLID:56;
( (SW-corner X) `2 <= (W-min X) `2 & (SW-corner X) `2 <= (W-max X) `2 & (W-min X) `2 <= (NW-corner X) `2 & (W-max X) `2 <= (NW-corner X) `2 ) by Th87;
then ( W-min X in LSeg (SW-corner X),(NW-corner X) & W-max X in LSeg (SW-corner X),(NW-corner X) ) by A1, GOBOARD7:8;
hence LSeg (W-min X),(W-max X) c= LSeg (SW-corner X),(NW-corner X) by TOPREAL1:12; :: thesis: verum