theorem Th2: :: SCMYCIEL:2

for x, X being object holds [x,X] <> X