let x, y, A be set ; :: thesis: ( <*x,y*> - A = {} iff ( x in A & y in A ) )
thus ( <*x,y*> - A = {} implies ( x in A & y in A ) ) :: thesis: ( x in A & y in A implies <*x,y*> - A = {} )

proof

assume <*x,y*> - A = {} ; :: thesis: ( x in A & y in A )
then rng <*x,y*> c= A by Th75;
then {x,y} c= A by FINSEQ_2:147;
hence ( x in A & y in A ) by ZFMISC_1:38; :: thesis: verum

end;

assume ( x in A & y in A ) ; :: thesis: <*x,y*> - A = {}
then ( <*x*> - A = {} & <*y*> - A = {} & <*x,y*> = <*x*> ^ <*y*> ) by Lm7, FINSEQ_1:def 9;
hence <*x,y*> - A = {} ^ {} by Lm11
.= {} by FINSEQ_1:47 ;
:: thesis: verum