let x, y be object ; :: thesis: for A being set st not x in A & y in A holds
<*x,y*> - A = <*x*>
let A be set ; :: thesis: ( not x in A & y in A implies <*x,y*> - A = <*x*> )
assume that
A1: not x in A and
A2: y in A ; :: thesis: <*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 ;
:: thesis: verum