let x be object ; :: thesis: for A being set holds
( <*x*> - A = {} iff x in A )
let A be set ; :: thesis: ( <*x*> - A = {} iff x in A )
A1: rng <*x*> = {x} by FINSEQ_1:39;
thus ( <*x*> - A = {} implies x in A ) :: thesis: ( x in A implies <*x*> - A = {} )

proof

assume <*x*> - A = {} ; :: thesis: x in A
then rng <*x*> c= A by Th66;
then {x} c= A by FINSEQ_1:39;
hence x in A by ZFMISC_1:31; :: thesis: verum

end;

assume x in A ; :: thesis: <*x*> - A = {}
then rng <*x*> c= A by A1, ZFMISC_1:31;
hence <*x*> - A = {} by Th66; :: thesis: verum