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