theorem Th17: :: TOPREAL1:17

(LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) = {|[0,0]|}