theorem Th23: :: HEYTING2:23

for V being set
for C being finite set
for a being finite Element of PFuncs (V,C) holds a in (Atom (V,C)) . a