let X be ARS ; ( ( for x, y, z being Element of X st x ==> y & y ==> z holds
x ==> z ) implies for x, y being Element of X st x =+=> y holds
x ==> y )
assume A1:
for x, y, z being Element of X st x ==> y & y ==> z holds
x ==> z
; for x, y being Element of X st x =+=> y holds
x ==> y
let x, y be Element of X; ( x =+=> y implies x ==> y )
assume A2:
x =+=> y
; x ==> y
consider z being Element of X such that
A3:
x ==> z
and
A4:
z =*=> y
by A2;
defpred S1[ Element of X] means x ==> $1;
A5:
S1[z]
by A3;
A6:
for u, v being Element of X st u ==> v & S1[u] holds
S1[v]
by A1;
thus
S1[y]
from ABSRED_0:sch 2(A4, A5, A6); verum