:: deftheorem defines pi_2143 ANPROJ10:def 6 :
for X being non empty set
for x being Tuple of 4,X holds pi_2143 x = <*(x . 2),(x . 1),(x . 4),(x . 3)*>;