:: deftheorem Def6 defines DnT REALSET1:def 6 :
for A being set
for x being Element of A
for b₃ being BinOp of A holds
( b₃ is DnT of x,A iff for y being set st y in [:(A \ {x}),(A \ {x}):] holds
b₃ . y in A \ {x} );