theorem Th3: :: SCMYCIEL:3
for x, X being object holds [x,X] <> x