:: deftheorem Def5 defines StrongImpl HEYTING2:def 5 :
for V being set
for C being finite set
for b₃ being BinOp of the carrier of (SubstLatt (V,C)) holds
( b₃ = StrongImpl (V,C) iff for u, v being Element of (SubstLatt (V,C))
for u9, v9 being Element of SubstitutionSet (V,C) st u9 = u & v9 = v holds
b₃ . (u,v) = mi (u9 =>> v9) );