theorem Th25: :: HEYTING2:25

for V being set
for C being finite set
for u, v being Element of (SubstLatt (V,C))
for a being finite Element of PFuncs (V,C) st ( for b being Element of PFuncs (V,C) st b in u holds
b tolerates a ) & u "/\" ((Atom (V,C)) . a) [= v holds
(Atom (V,C)) . a [= (StrongImpl (V,C)) . (u,v)