let p, q be Point of (TOP-REAL 2); :: thesis: L~ <*p,q*> = LSeg (p,q)
set f = <*p*>;
A1: len <*p*> = 1 by FINSEQ_1:39;
thus L~ <*p,q*> = L~ (<*p*> ^ <*q*>) by FINSEQ_1:def 9
.= (L~ <*p*>) \/ (LSeg ((<*p*> /. (len <*p*>)),q)) by Th19
.= (L~ <*p*>) \/ (LSeg (p,q)) by A1, FINSEQ_4:16
.= {} \/ (LSeg (p,q)) by A1, TOPREAL1:22
.= LSeg (p,q) ; :: thesis: verum