theorem :: ABSRED_0:153

for X being ARS holds
( X is WCR iff the reduction of X is locally-confluent )