:: deftheorem Def9 defines quadruple XTUPLE_0:def 9 :
for x being object holds
( x is quadruple iff ex x1, x2, x3, x4 being object st x = [x1,x2,x3,x4] );