theorem Th48: :: MCART_1:62
for X, Y being set st [:X,Y:] <> {} holds
for x being Element of [:X,Y:] holds
( x <> x `1 & x <> x `2 )