theorem Th14: :: MCART_1:20

for x being object st ex y, z being object st x = [y,z] holds
( x <> x `1 & x <> x `2 )