theorem Th20: :: HEYTING2:20

for V being set
for C being finite set
for u, v being Element of (SubstLatt (V,C)) holds (diff u) . v [= u