for x being set holds x is_a_normal_form_wrt {} ;