theorem Th3: :: RECDEF_2:3

for z being object
for A, B, C being set st z in [:A,B,C:] holds
z = [(z `1_3),(z `2_3),(z `3_3)]