:: deftheorem defines subcommutative REWRITE1:def 21 :
for R being Relation holds
( R is subcommutative iff for a, b, c being object st [a,b] in R & [a,c] in R holds
b,c are_convergent<=1_wrt R );