theorem Th18: :: MCART_1:24

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