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