:: deftheorem Def5 defines triple XTUPLE_0:def 5 :
for x being object holds
( x is triple iff ex x1, x2, x3 being object st x = [x1,x2,x3] );