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

( 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