let x, A be set ; :: thesis: ( <*x*> - A = <*x*> iff not x in A )
thus ( <*x*> - A = <*x*> implies not x in A ) :: thesis: ( not x in A implies <*x*> - A = <*x*> )

proof

assume <*x*> - A = <*x*> ; :: thesis: not x in A
then ( x in {x} & rng <*x*> = {x} & rng <*x*> misses A ) by Th76, FINSEQ_1:56, TARSKI:def 1;
hence not x in A by XBOOLE_0:3; :: thesis: verum

end;

assume A1: not x in A ; :: thesis: <*x*> - A = <*x*>
rng <*x*> misses A

proof

assume rng <*x*> meets A ; :: thesis: contradiction
then consider y being set such that
A2: ( y in rng <*x*> & y in A ) by XBOOLE_0:3;
y in {x} by A2, FINSEQ_1:56;
hence contradiction by A1, A2, TARSKI:def 1; :: thesis: verum

end;

hence <*x*> - A = <*x*> by Th76; :: thesis: verum