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

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