theorem :: PSCOMP_1:33

for X being non empty compact Subset of (TOP-REAL 2) holds LSeg ((W-min X),(W-max X)) c= LSeg ((SW-corner X),(NW-corner X))