let p, q, r be Point of (TOP-REAL 2); :: thesis: L~ <*p,q,r*> = (LSeg p,q) \/ (LSeg q,r)
A1: <*p,q*> /. 2 = q by FINSEQ_4:26;
A2: <*r*> /. 1 = r by FINSEQ_4:25;
A3: <*p,q,r*> = <*p,q*> ^ <*r*> by FINSEQ_1:60;
len <*p,q*> = 2 by FINSEQ_1:61;
hence L~ <*p,q,r*> = ((L~ <*p,q*>) \/ (LSeg q,r)) \/ (L~ <*r*>) by A1, A2, A3, SPPOL_2:23
.= ((L~ <*p,q*>) \/ (LSeg q,r)) \/ {} by SPPOL_2:12
.= (LSeg p,q) \/ (LSeg q,r) by SPPOL_2:21 ;
:: thesis: verum