let X be ARS ; :: thesis: ( ( for x, y being Element of X st x ==> y holds

y ==> x ) implies for x, y being Element of X st x <=*=> y holds

x =*=> y )

assume A: for x, y being Element of X st x ==> y holds

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

defpred S_{1}[ Element of X] means x =*=> $1;

C: for u, v being Element of X st u <==> v & S_{1}[u] holds

S_{1}[v]
by A, Lem10;

D: for u, v being Element of X st u <=*=> v & S_{1}[u] holds

S_{1}[v]
from ABSRED_0:sch 5(C);

thus x =*=> y by B, D; :: thesis: verum

y ==> x ) implies for x, y being Element of X st x <=*=> y holds

x =*=> y )

assume A: for x, y being Element of X st x ==> y holds

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

defpred S

C: for u, v being Element of X st u <==> v & S

S

D: for u, v being Element of X st u <=*=> v & S

S

thus x =*=> y by B, D; :: thesis: verum