theorem :: FINSEQ_3:76

for x being object
for A being set holds
( <*x*> - A = {} iff x in A ) by Lm7;