let x, y be Real; :: thesis: <*x,y*> is Point of
reconsider x1 = x, y1 = y as Element of REAL ;
<*x1,y1*> in REAL 2 by FINSEQ_2:121;
hence <*x,y*> is Point of by REAL_NS1:def 4; :: thesis: verum