let x, A be set ; :: thesis: ( <*x*> - A = {} iff x in A )
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 Th75;
then {x} c= A by FINSEQ_1:56;
hence x in A by ZFMISC_1:37; :: thesis: verum

end;

assume A1: x in A ; :: thesis: <*x*> - A = {}
rng <*x*> = {x} by FINSEQ_1:56;
then rng <*x*> c= A by A1, ZFMISC_1:37;
hence <*x*> - A = {} by Th75; :: thesis: verum