theorem :: FINSEQ_3:75
for x being object
for A being set holds
( <*x*> - A = <*x*> iff not x in A ) by Lm6;