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 Th24;
len <*x,y*> = 2 by FINSEQ_1:61;
hence <*x,y*> |-- y = {} by A1, A2, FINSEQ_4:64; :: thesis: verum