theorem :: NORMFORM:31

for A being set holds {} in Normal_forms_on A by Lm4;