theorem Th30: :: SPRECT_1:30

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