let R be Relation; :: thesis: for a, b, c being set st a,b are_convertible_wrt R & b,c are_convertible_wrt R holds
a,c are_convertible_wrt R
let a, b, c be set ; :: thesis: ( a,b are_convertible_wrt R & b,c are_convertible_wrt R implies a,c are_convertible_wrt R )
assume ( R \/ (R ~) reduces a,b & R \/ (R ~) reduces b,c ) ; :: according to REWRITE1:def 4 :: thesis: a,c are_convertible_wrt R
hence R \/ (R ~) reduces a,c by Th17; :: according to REWRITE1:def 4 :: thesis: verum