:: deftheorem Def4 defines pseudo_compl HEYTING2:def 4 :
for V being set
for C being finite set
for b₃ being UnOp of the carrier of (SubstLatt (V,C)) holds
( b₃ = pseudo_compl (V,C) iff for u being Element of (SubstLatt (V,C))
for u9 being Element of SubstitutionSet (V,C) st u9 = u holds
b₃ . u = mi (- u9) );