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