theorem Th13: :: HEYTING1:13

for A being set
for K being Element of Normal_forms_on A st K = {} holds
- K = {[{},{}]}