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