let x, y, 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 )
A3: <*x*> = (<*x*> ^ <*y*>) - A by A1, FINSEQ_1:def 9
.= (<*x*> - A) ^ (<*y*> - A) by Lm11 ;
A4: ( ( x in A implies <*x*> - A = {} ) & ( not x in A implies <*x*> - A = <*x*> ) & ( y in A implies <*y*> - A = {} ) & ( not y in A implies <*y*> - A = <*y*> ) ) by Lm6, Lm7;
assume ( x in A or not y in A ) ; :: thesis: contradiction
then ( <*x*> = {} or <*x*> = <*y*> or <*x*> = <*x,y*> ) by A3, A4, FINSEQ_1:47, FINSEQ_1:def 9;
then ( <*x*> = <*y*> & <*x*> . 1 = x & <*y*> . 1 = y ) by Th40, FINSEQ_1:57;
hence contradiction by A2; :: thesis: verum