for V being set
for C being finite set
for u, v being Element of (SubstLatt (V,C)) holds u "/\" ((StrongImpl (V,C)) . (u,v)) [= v