theorem :: PSCOMP_1:35

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