theorem Th35: :: MCART_1:47

for X1, X2, X3 being non empty set
for x being Element of [:X1,X2,X3:] holds
( x <> x `1_3 & x <> x `2_3 & x <> x `3_3 )