theorem :: TOPREAL1:16

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