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