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