let R be Relation; :: thesis: for a, b being set st [a,b] in R holds
a,b are_convertible_wrt R
let a, b be set ; :: thesis: ( [a,b] in R implies a,b are_convertible_wrt R )
assume [a,b] in R ; :: thesis: a,b are_convertible_wrt R
then R reduces a,b by Th16;
hence a,b are_convertible_wrt R by Th26; :: thesis: verum