let x, y be set ; :: thesis: ( x <> y implies <*x,y*> |-- y = {} )

y in {x,y} by TARSKI:def 2;

then A1: y in rng <*x,y*> by Lm1;

assume x <> y ; :: thesis: <*x,y*> |-- y = {}

then A2: y .. <*x,y*> = 2 by Th20;

len <*x,y*> = 2 by FINSEQ_1:44;

hence <*x,y*> |-- y = {} by A1, A2, FINSEQ_4:49; :: thesis: verum

y in {x,y} by TARSKI:def 2;

then A1: y in rng <*x,y*> by Lm1;

assume x <> y ; :: thesis: <*x,y*> |-- y = {}

then A2: y .. <*x,y*> = 2 by Th20;

len <*x,y*> = 2 by FINSEQ_1:44;

hence <*x,y*> |-- y = {} by A1, A2, FINSEQ_4:49; :: thesis: verum