theorem Th24: :: HEYTING1:24

for A being set
for u, v being Element of (NormForm A) holds u "/\" ((StrongImpl A) . (u,v)) [= v