let X be ARS ; :: thesis: for x, y being Element of X st x <==> y holds
x <=*=> y
let x, y be Element of X; :: thesis: ( x <==> y implies x <=*=> y )
assume ( x ==> y or x <== y ) ; :: according to ABSRED_0:def 5 :: thesis: x <=*=> y
hence x,y are_convertible_wrt the reduction of X by REWRITE1:29, REWRITE1:31; :: according to ABSRED_0:def 7 :: thesis: verum