let x, y be object ; :: thesis: for A being set st <*x,y*> - A = <*y*> & x <> y holds
( x in A & not y in A )
let A be set ; :: thesis: ( <*x,y*> - A = <*y*> & x <> y implies ( x in A & not y in A ) )
assume that
A1: <*x,y*> - A = <*y*> and
A2: x <> y ; :: thesis: ( x in A & not y in A )
assume A3: ( not x in A or 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 by FINSEQ_1:40;
<*y*> = (<*x*> ^ <*y*>) - A by A1, FINSEQ_1:def 9
.= (<*x*> - A) ^ (<*y*> - A) by Lm11 ;
then ( <*y*> = {} or <*x*> = <*y*> or <*y*> = <*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