let R be Relation; :: thesis: for a, b being object st [a,b] in R holds
a,b are_convertible_wrt R
let a, b be object ; :: 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 Th15;
hence a,b are_convertible_wrt R by Th25; :: thesis: verum