let x, y be object ; :: thesis: for A being set holds
( <*x,y*> - A = <*x,y*> iff ( not x in A & not y in A ) )
let A be set ; :: thesis: ( <*x,y*> - A = <*x,y*> iff ( not x in A & not y in A ) )
A1: <*x,y*> = <*x*> ^ <*y*> by FINSEQ_1:def 9;
thus ( <*x,y*> - A = <*x,y*> implies ( not x in A & not y in A ) ) :: thesis: ( not x in A & not y in A implies <*x,y*> - A = <*x,y*> )
proof
assume A2: <*x,y*> - A = <*x,y*> ; :: thesis: ( not x in A & not y in A )
assume ( x in A or y in A ) ; :: thesis: contradiction
then ( ( x in A & y in A ) or ( not x in A & y in A ) or ( x in A & not y in A ) ) ;
then ( <*x,y*> - A = {} or <*x,y*> - A = <*x*> or <*x,y*> - A = <*y*> ) by Th75, Th76, Th78;
hence contradiction by A2, Th33; :: thesis: verum
end;
assume that
A3: not x in A and
A4: not y in A ; :: thesis: <*x,y*> - A = <*x,y*>
A5: <*y*> - A = <*y*> by A4, Lm6;
<*x*> - A = <*x*> by A3, Lm6;
hence <*x,y*> - A = <*x,y*> by A5, A1, Lm11; :: thesis: verum