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₁[ Element of X] means x =*=> $1;
C: for u, v being Element of X st u <==> v & S₁[u] holds
S₁[v] by A, Lem10;
D: for u, v being Element of X st u <=*=> v & S₁[u] holds
S₁[v] from ABSRED_0:sch 5(C);
thus x =*=> y by B, D; :: thesis: verum