:: deftheorem Def1 defines pair XTUPLE_0:def 1 :
for x being object holds
( x is pair iff ex x1, x2 being object st x = [x1,x2] );