theorem :: ANPROJ10:10

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