:: deftheorem Def7 defines diff HEYTING2:def 7 :
for V being set
for C being finite set
for u being Element of (SubstLatt (V,C))
for b₄ being UnOp of the carrier of (SubstLatt (V,C)) holds
( b₄ = diff u iff for v being Element of (SubstLatt (V,C)) holds b₄ . v = u \ v );