let U be Universe; :: thesis: for x being Element of U
for x1, x2, x3 being object st x = [x1,x2,x3] holds
( x1 is Element of U & x2 is Element of U & x3 is Element of U )
let x be Element of U; :: thesis: for x1, x2, x3 being object st x = [x1,x2,x3] holds
( x1 is Element of U & x2 is Element of U & x3 is Element of U )
let x1, x2, x3 be object ; :: thesis: ( x = [x1,x2,x3] implies ( x1 is Element of U & x2 is Element of U & x3 is Element of U ) )
assume x = [x1,x2,x3] ; :: thesis: ( x1 is Element of U & x2 is Element of U & x3 is Element of U )
then x = [[x1,x2],x3] by XTUPLE_0:def 4;
then ( x3 is Element of U & [x1,x2] is Element of U ) by CLASSES4:22;
hence ( x1 is Element of U & x2 is Element of U & x3 is Element of U ) by CLASSES4:22; :: thesis: verum