let x, y be set ; :: thesis: ( x <> y implies <*x,y*> -| y = <*x*> )
assume x <> y ; :: thesis: <*x,y*> -| y = <*x*>
then y .. <*x,y*> = 1 + 1 by Th20;
then A1: 1 = (y .. <*x,y*>) - 1 ;
rng <*x,y*> = {x,y} by Lm1;
then y in rng <*x,y*> by TARSKI:def 2;
hence <*x,y*> -| y = <*x,y*> | (Seg 1) by A1, FINSEQ_4:33
.= <*x*> by Th3 ;
:: thesis: verum