let x, t be Real; :: thesis: <*x,t*> in REAL 2
P1: 2 -tuples_on REAL = { <*d1,d2*> where d1, d2 is Element of REAL : verum } by FINSEQ_2:99;
( x in REAL & t in REAL ) by XREAL_0:def 1;
hence <*x,t*> in REAL 2 by P1; :: thesis: verum