let R be Relation; :: thesis: ( R is empty implies R is subcommutative )
assume A1: R is empty ; :: thesis: R is subcommutative
let x be set ; :: according to REWRITE1:def 21 :: thesis: for b, c being set st [x,b] in R & [x,c] in R holds
b,c are_convergent<=1_wrt R
thus for b, c being set st [x,b] in R & [x,c] in R holds
b,c are_convergent<=1_wrt R by A1; :: thesis: verum