let U be Universe; :: thesis: for x1, x2, x3, x4, x5 being Element of U holds [x1,x2,x3,x4,x5] is Element of U
let x1, x2, x3, x4, x5 be Element of U; :: thesis: [x1,x2,x3,x4,x5] is Element of U
( [x1,x2,x3,x4] is Element of U & [x1,x2,x3,x4,x5] = [[x1,x2,x3,x4],x5] ) by GRCAT_1:1;
hence [x1,x2,x3,x4,x5] is Element of U by CLASSES2:58; :: thesis: verum