theorem Th5: :: HEYTING1:5

for A being set
for u being Element of (NormForm A)
for X being set st X c= u holds
X is Element of (NormForm A)