ex u1, u2 being object st u = [u1,u2] by XTUPLE_0:def 1;
hence u `1 is Element of UN by Th35; :: thesis: verum