theorem Th3: :: SCMYCIEL:3

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