:: deftheorem defines `2_4 RECDEF_2:def 5 :
for x being quadruple object
for b<sub>2</sub> being object holds
( b<sub>2</sub> = x `2_4 iff for y1, y2, y3, y4 being object st x = [y1,y2,y3,y4] holds
b₂ = y2 );