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