theorem Th93: :: FINSEQ_3:95

for x, y, z being object holds
( ( x <> y & y <> z & z <> x ) iff <*x,y,z*> is one-to-one )