let X be non empty ARS ; ( X is COMP iff the reduction of X is complete )
set R = the reduction of X;
A2:
( X is CONF iff the reduction of X is confluent )
by Ch17;
( X is SN iff the reduction of X is strongly-normalizing )
by Ch7, Ch8;
hence
( X is COMP iff the reduction of X is complete )
by A2; verum