let R be Relation; for a, b being object st [a,b] in R holds
a,b are_convertible_wrt R
let a, b be object ; ( [a,b] in R implies a,b are_convertible_wrt R )
assume
[a,b] in R
; a,b are_convertible_wrt R
then
R reduces a,b
by Th15;
hence
a,b are_convertible_wrt R
by Th25; verum