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