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