theorem :: MSAFREE4:78

for x being set holds x is_a_normal_form_wrt {} ;