let X be ARS ; :: thesis: ( X is CONF iff the reduction of X is confluent )
set R = the reduction of X;
set A = the carrier of X;
F0: field the reduction of X c= the carrier of X \/ the carrier of X by RELSET_1:8;
thus ( X is CONF implies the reduction of X is confluent ) :: thesis: ( the reduction of X is confluent implies X is CONF )

proof

assume A1: for x, y being Element of X st x <<>> y holds
x >><< y ; :: according to ABSRED_0:def 25 :: thesis: the reduction of X is confluent
let a, b be object ; :: according to REWRITE1:def 22 :: thesis: ( not a,b are_divergent_wrt the reduction of X or a,b are_convergent_wrt the reduction of X )
assume A2: a,b are_divergent_wrt the reduction of X ; :: thesis: a,b are_convergent_wrt the reduction of X
then A3: a,b are_convertible_wrt the reduction of X by REWRITE1:37;

per cases ( ( a in field the reduction of X & b in field the reduction of X ) or a = b ) by A3, REWRITE1:32;

suppose ( a in field the reduction of X & b in field the reduction of X ) ; :: thesis: a,b are_convergent_wrt the reduction of X

then reconsider x = a, y = b as Element of X by F0;
x <<>> y by A2, Ch11;
hence a,b are_convergent_wrt the reduction of X by A1, Ch12; :: thesis: verum

end;

suppose a = b ; :: thesis: a,b are_convergent_wrt the reduction of X

hence a,b are_convergent_wrt the reduction of X by REWRITE1:38; :: thesis: verum

end;

end;

end;

assume A5: for a, b being object st a,b are_divergent_wrt the reduction of X holds
a,b are_convergent_wrt the reduction of X ; :: according to REWRITE1:def 22 :: thesis: X is CONF
let x be Element of X; :: according to ABSRED_0:def 25 :: thesis: for y being Element of X st x <<>> y holds
x >><< y
let y be Element of X; :: thesis: ( x <<>> y implies x >><< y )
assume x <<>> y ; :: thesis: x >><< y
then x,y are_divergent_wrt the reduction of X by Ch11;
hence x >><< y by A5, Ch12; :: thesis: verum