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