theorem Th14: :: HEYTING1:14

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