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