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:56;
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:25
.= {} \/ (LSeg p,q) by A1, TOPREAL1:28
.= LSeg p,q ; :: thesis: verum