theorem Th29: :: SPRECT_1:29

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