theorem Th17: :: HEYTING1:17

for A being set holds {[{},{}]} is Element of Normal_forms_on A