theorem Th4: :: HEYTING1:4

for A being set
for K being Element of Normal_forms_on A
for X being set st X c= K holds
X in Normal_forms_on A