let a be Real; :: thesis: <*a*> is Point of (Euclid 1)
reconsider ra = <*a*> as FinSequence of REAL ;
dom ra = Seg 1 by FINSEQ_1:def 8;
then len ra = 1 by FINSEQ_1:def 3;
hence <*a*> is Point of (Euclid 1) by TOPREAL3:45; :: thesis: verum