let x, y, z be set ; :: thesis: ( x <> z & y <> z implies <*x,y,z*> |-- z = {} )
assume that
A1: x <> z and
A2: y <> z ; :: thesis: <*x,y,z*> |-- z = {}
A3: len <*x,y,z*> = 3 by FINSEQ_1:45;
z in {x,y,z} by ENUMSET1:def 1;
then A4: z in rng <*x,y,z*> by Lm2;
z .. <*x,y,z*> = 3 by A1, A2, Th23;
hence <*x,y,z*> |-- z = {} by A4, A3, FINSEQ_4:49; :: thesis: verum