let x, z, y be set ; :: thesis: ( x <> z & y <> z implies <*x,y,z*> |-- z = {} )
z in {x,y,z} by ENUMSET1:def 1;
then A1: z in rng <*x,y,z*> by Lm2;
assume ( x <> z & y <> z ) ; :: thesis: <*x,y,z*> |-- z = {}
then ( z .. <*x,y,z*> = 3 & len <*x,y,z*> = 3 ) by Th27, FINSEQ_1:62;
hence <*x,y,z*> |-- z = {} by A1, FINSEQ_4:64; :: thesis: verum