let p, q be Point of (TOP-REAL 2); :: thesis: <*p,q*> is unfolded
len <*p,q*> = 2 by FINSEQ_1:44;
hence <*p,q*> is unfolded by Th26; :: thesis: verum