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