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

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