theorem :: TOPREAL3:16

for p1, p2, p3 being Point of (TOP-REAL 2)
for f being FinSequence of (TOP-REAL 2) st f = <*p1,p2,p3*> holds
L~ f = (LSeg (p1,p2)) \/ (LSeg (p2,p3))