let x, y be object ; for A being set st not x in A & y in A holds
<*x,y*> - A = <*x*>
let A be set ; ( not x in A & y in A implies <*x,y*> - A = <*x*> )
assume that
A1:
not x in A
and
A2:
y in A
; <*x,y*> - A = <*x*>
A3:
<*y*> - A = {}
by A2, Lm7;
A4:
<*x,y*> = <*x*> ^ <*y*>
by FINSEQ_1:def 9;
<*x*> - A = <*x*>
by A1, Lm6;
hence <*x,y*> - A =
<*x*> ^ {}
by A3, A4, Lm11
.=
<*x*>
by FINSEQ_1:34
;
verum