:: deftheorem Def3 defines `2 XTUPLE_0:def 3 :
for x being object st x is pair holds
for b<sub>2</sub> being object holds
( b<sub>2</sub> = x `2 iff for y1, y2 being object st x = [y1,y2] holds
b₂ = y2 );