theorem Th33: :: FINSEQ_3:35

for x, y, z being object holds <*x*> <> <*y,z*>