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