let x, y, z be set ; :: thesis: ( ( x <> y & y <> z & z <> x ) iff <*x,y,z*> is one-to-one )
thus ( x <> y & y <> z & z <> x implies <*x,y,z*> is one-to-one ) :: thesis: ( <*x,y,z*> is one-to-one implies ( x <> y & y <> z & z <> x ) )

proof

assume that
A1: x <> y and
A2: ( y <> z & z <> x ) ; :: thesis: <*x,y,z*> is one-to-one
{x,y} /\ {z} = {}

proof

assume A3: not {x,y} /\ {z} = {} ; :: thesis: contradiction
consider y1 being Element of {x,y} /\ {z};
( y1 in {x,y} & y1 in {z} ) by A3, XBOOLE_0:def 4;
then ( ( y1 = x or y1 = y ) & y1 = z ) by TARSKI:def 1, TARSKI:def 2;
hence contradiction by A2; :: thesis: verum

end;

then {} = (rng <*x,y*>) /\ {z} by FINSEQ_2:147
.= (rng <*x,y*>) /\ (rng <*z*>) by FINSEQ_1:55 ;
then A4: rng <*x,y*> misses rng <*z*> by XBOOLE_0:def 7;
( <*x,y*> is one-to-one & <*z*> is one-to-one ) by A1, Th102, Th103;
then <*x,y*> ^ <*z*> is one-to-one by A4, Th98;
hence <*x,y,z*> is one-to-one by FINSEQ_1:60; :: thesis: verum

end;

set p = <*x,y,z*>;
assume A5: <*x,y,z*> is one-to-one ; :: thesis: ( x <> y & y <> z & z <> x )
( 1 in {1,2,3} & 2 in {1,2,3} & 3 in {1,2,3} ) by ENUMSET1:def 1;
then ( 1 in dom <*x,y,z*> & 2 in dom <*x,y,z*> & 3 in dom <*x,y,z*> & 1 <> 2 & 1 <> 3 & 2 <> 3 & <*x,y,z*> . 1 = x & <*x,y,z*> . 2 = y & <*x,y,z*> . 3 = z ) by Th1, Th30, FINSEQ_1:62;
hence ( x <> y & y <> z & z <> x ) by A5, FUNCT_1:def 8; :: thesis: verum