theorem :: PSCOMP_1:51

for X being non empty compact Subset of (TOP-REAL 2) holds
( (LSeg ((SE-corner X),(E-min X))) /\ X = {(E-min X)} & (LSeg ((E-max X),(NE-corner X))) /\ X = {(E-max X)} )