let R be Relation; :: thesis: ( R is subcommutative implies R is confluent )
assume R is subcommutative ; :: thesis: R is confluent
then for a, b, c being object st R reduces a,b & [a,c] in R holds
b,c are_convergent_wrt R by Th49;
hence R is confluent by Th51; :: thesis: verum