let UN be Universe; 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; ( [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; verum