let x, y, A be set ; :: thesis: ( <*x,y*> - A = <*x,y*> iff ( not x in A & not y in A ) )
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 A1: <*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 Th84, Th85, Th87;
hence contradiction by A1, Th38, Th40; :: thesis: verum

end;

assume ( not x in A & not y in A ) ; :: thesis: <*x,y*> - A = <*x,y*>
then ( <*x*> - A = <*x*> & <*y*> - A = <*y*> & <*x,y*> = <*x*> ^ <*y*> ) by Lm6, FINSEQ_1:def 9;
hence <*x,y*> - A = <*x,y*> by Lm11; :: thesis: verum