let X be ARS ; :: thesis: for x, y being Element of X holds
( x <=+=> y iff ex z being Element of X st
( x <=*=> z & z <==> y ) )
let x, y be Element of X; :: thesis: ( x <=+=> y iff ex z being Element of X st
( x <=*=> z & z <==> y ) )
( x <=+=> y iff ex z being Element of X st
( y <==> z & z <=*=> x ) ) by Def8;
hence ( x <=+=> y iff ex z being Element of X st
( x <=*=> z & z <==> y ) ) ; :: thesis: verum