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