let D be non empty set ; for p1, p2 being Element of D st p1 <> p2 holds
<*p1,p2*> :- p2 = <*p2*>
let p1, p2 be Element of D; ( p1 <> p2 implies <*p1,p2*> :- p2 = <*p2*> )
assume A1:
p1 <> p2
; <*p1,p2*> :- p2 = <*p2*>
p2 in {p1,p2}
by TARSKI:def 2;
then
p2 in rng <*p1,p2*>
by Lm1;
hence <*p1,p2*> :- p2 =
<*p2*> ^ (<*p1,p2*> |-- p2)
by Th41
.=
<*p2*> ^ {}
by A1, Th33
.=
<*p2*>
by FINSEQ_1:34
;
verum