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