let x, y, z be set ; :: thesis: ( x <> y implies <*x,y,z*> -| y = <*x*> )
assume x <> y ; :: thesis: <*x,y,z*> -| y = <*x*>
then y .. <*x,y,z*> = 1 + 1 by Th22;
then A1: 1 = (y .. <*x,y,z*>) - 1 ;
rng <*x,y,z*> = {x,y,z} by Lm2;
then y in rng <*x,y,z*> by ENUMSET1:def 1;
hence <*x,y,z*> -| y = <*x,y,z*> | (Seg 1) by A1, FINSEQ_4:33
.= <*x*> by Th4 ;
:: thesis: verum