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