theorem :: SPRECT_1:27

for C being non empty compact Subset of (TOP-REAL 2) holds (LSeg ((SW-corner C),(NW-corner C))) /\ (LSeg ((NW-corner C),(NE-corner C))) = {(NW-corner C)}