theorem Th19: :: HEYTING2:19

for V being set
for C being finite set
for u being Element of SubstitutionSet (V,C) holds u = FinJoin (u,(Atom (V,C)))