:: deftheorem Def7 defines `4 CLASSES5:def 6 :
for x being object st x is quintuple holds
for b<sub>2</sub> being object holds
( b<sub>2</sub> = x `4 iff for y1, y2, y3, y4, y5 being object st x = [y1,y2,y3,y4,y5] holds
b₂ = y4 );