:: deftheorem Def8 defines pseudo_compl HEYTING1:def 8 :
for A being set
for b₂ being UnOp of the carrier of (NormForm A) holds
( b₂ = pseudo_compl A iff for u being Element of (NormForm A) holds b₂ . u = mi (- (@ u)) );