ex a, b being object st
( a in REAL & b in REAL & x = [a,b] ) by ZFMISC_1:def 2;
hence x `1 is Element of REAL ; :: thesis: verum