let x, y be object ; :: thesis: for A being set holds
( <*x,y*> - A = {} iff ( x in A & y in A ) )
let 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 Th66;
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;
<*x*> - A = {} by A2, Lm7;
hence <*x,y*> - A = {} ^ {} by A4, A1, Lm11
.= {} ;
:: thesis: verum