let p, q be Point of ; :: thesis: <*p,q*> is unfolded
len <*p,q*> = 2 by FINSEQ_1:61;
hence <*p,q*> is unfolded by Th27; :: thesis: verum