theorem Th14: :: CLASSES5:14
for U being Universe
for x being Element of U
for x1, x2, x3, x4, x5 being object st x = [x1,x2,x3,x4,x5] holds
( x1 is Element of U & x2 is Element of U & x3 is Element of U & x4 is Element of U & x5 is Element of U )