theorem :: PSCOMP_1:49
for X being non empty compact Subset of (TOP-REAL 2) holds LSeg ((E-min X),(E-max X)) c= LSeg ((SE-corner X),(NE-corner X))