theorem :: PSCOMP_1:59

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