let UN be Universe; :: thesis: for u1, u2, u3, u4 being Element of UN holds
( [u1,u2,u3] in UN & [u1,u2,u3,u4] in UN )
let u1, u2, u3, u4 be Element of UN; :: thesis: ( [u1,u2,u3] in UN & [u1,u2,u3,u4] in UN )
( [u1,u2,u3] = [[u1,u2],u3] & [u1,u2,u3,u4] = [[u1,u2,u3],u4] ) ;
hence ( [u1,u2,u3] in UN & [u1,u2,u3,u4] in UN ) by CLASSES2:58; :: thesis: verum