( x is Real & y is Real ) by XREAL_0:def 1;
hence <*x,y*> is Point of (TOP-REAL 2) by FINSEQ_2:121; :: thesis: verum