let x be object ; :: thesis: for A being set holds
( <*x*> - A = <*x*> iff not x in A )
let 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 A1: rng <*x*> misses A by Th67;
A2: rng <*x*> = {x} by FINSEQ_1:39;
x in {x} by TARSKI:def 1;
hence not x in A by A2, A1, XBOOLE_0:3; :: thesis: verum
end;
assume A3: not x in A ; :: thesis: <*x*> - A = <*x*>
rng <*x*> misses A
proof
assume rng <*x*> meets A ; :: thesis: contradiction
then consider y being object such that
A4: y in rng <*x*> and
A5: y in A by XBOOLE_0:3;
y in {x} by A4, FINSEQ_1:39;
hence contradiction by A3, A5, TARSKI:def 1; :: thesis: verum
end;
hence <*x*> - A = <*x*> by Th67; :: thesis: verum