:: deftheorem Def11 defines diff HEYTING1:def 11 :
for A being set
for u being Element of (NormForm A)
for b₃ being UnOp of the carrier of (NormForm A) holds
( b₃ = diff u iff for v being Element of (NormForm A) holds b₃ . v = u \ v );