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 A1: x <<>> y ; :: thesis: x <=*=> y

consider u being Element of X such that

A2: ( x <=*= u & u =*=> y ) by A1;

A3: ( x <=*=> u & u <=*=> y ) by A2, Lm3;

thus x <=*=> y by A3, Th7; :: thesis: verum

x <=*=> y

let x, y be Element of X; :: thesis: ( x <<>> y implies x <=*=> y )

assume A1: x <<>> y ; :: thesis: x <=*=> y

consider u being Element of X such that

A2: ( x <=*= u & u =*=> y ) by A1;

A3: ( x <=*=> u & u <=*=> y ) by A2, Lm3;

thus x <=*=> y by A3, Th7; :: thesis: verum