let p be Point of ; :: thesis: L~ <*p*> = {}
len <*p*> = 1 by FINSEQ_1:56;
hence L~ <*p*> = {} by TOPREAL1:28; :: thesis: verum