let R be Relation; :: thesis: for a being set holds a,a are_convertible_wrt R
let a be set ; :: thesis: a,a are_convertible_wrt R
R reduces a,a by Th13;
hence a,a are_convertible_wrt R by Th26; :: thesis: verum