theorem Th26: :: HEYTING2:26

for V being set
for C being finite set
for u being Element of (SubstLatt (V,C)) holds u "/\" ((pseudo_compl (V,C)) . u) = Bottom (SubstLatt (V,C))