for X being ARS
for x being Element of X holds
( x is normalizable iff x has_a_normal_form_wrt the reduction of X )