theorem Th17: :: HEYTING2:17

for V being set
for C being finite set
for u being Element of (SubstLatt (V,C))
for X being set st X c= u holds
X is Element of (SubstLatt (V,C))