theorem :: ABSRED_0:152

for X being ARS holds
( X is CR iff the reduction of X is with_Church-Rosser_property )