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:17;
A2: <*r*> /. 1 = r by FINSEQ_4:16;
A3: <*p,q,r*> = <*p,q*> ^ <*r*> by FINSEQ_1:43;
len <*p,q*> = 2 by FINSEQ_1:44;
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