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