:: deftheorem Def9 defines StrongImpl HEYTING1:def 9 :
for A being set
for b₂ being BinOp of the carrier of (NormForm A) holds
( b₂ = StrongImpl A iff for u, v being Element of (NormForm A) holds b₂ . (u,v) = mi ((@ u) =>> (@ v)) );