let x, 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 Th75;
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 Th75; :: thesis: verum