let x, y, A be set ; :: thesis: ( <*x,y*> - A = {} iff ( x in A & y in A ) )
A1: <*x,y*> = <*x*> ^ <*y*> by FINSEQ_1:def 9;
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:127;
hence ( x in A & y in A ) by ZFMISC_1:32; :: thesis: verum

end;

assume that
A2: x in A and
A3: y in A ; :: thesis: <*x,y*> - A = {}
A4: <*y*> - A = {} by A3, Lm7;
(card {}) + (card {}) = card ({} ^ {}) by FINSEQ_1:22;
then xx: card ({} ^ {}) = 0 ;
<*x*> - A = {} by A2, Lm7;
hence <*x,y*> - A = {} ^ {} by A4, A1, Lm11
.= {} by xx ;
:: thesis: verum