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

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