let x, y be object ; for A being set st <*x,y*> - A = <*x*> & x <> y holds
( not x in A & y in A )
let A be set ; ( <*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
; ( not x in A & y in A )
assume A3:
( x in A or not y in A )
; 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;
<*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; verum