theorem :: PSCOMP_1:43

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