theorem Ch1: :: ABSRED_0:91

for X being ARS
for x being Element of X holds
( x is normform iff x is_a_normal_form_wrt the reduction of X )