theorem :: MCART_1:63

for x being object
for X, Y being set st x in [:X,Y:] holds
( x <> x `1 & x <> x `2 ) by Th48;