:: deftheorem defines `3_3 MCART_1:def 7 :
for X1, X2, X3 being non empty set
for x being Element of [:X1,X2,X3:]
for b<sub>5</sub> being Element of X3 holds
( b<sub>5</sub> = x `3_3 iff for x1, x2, x3 being object st x = [x1,x2,x3] holds
b₅ = x3 );