theorem :: ABCMIZ_A:1

for x being pair object holds x = [(x `1),(x `2)] ;