theorem :: ANPROJ10:9

for X being non empty set
for x being Tuple of 4,X holds
( pi_13 (pi_23 (pi_13 x)) = pi_12 x & pi_12 (pi_34 (pi_23 (pi_13 x))) = pi_34 (pi_23 x) & pi_23 (pi_24 (pi_14 (pi_23 (pi_13 x)))) = pi_14 x ) ;