theorem :: TOPREAL1:15

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