for n being Element of NAT
for p1, p2 being Point of (TOP-REAL n) st p1 <> p2 holds
I[01] ,(TOP-REAL n) | (LSeg (p1,p2)) are_homeomorphic by Th37, TOPREAL1:9;