let X be ARS ; :: thesis: ( ( 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 ; :: 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 A2: x =+=> y ; :: thesis: x ==> y

consider z being Element of X such that

A3: x ==> z and

A4: z =*=> y by A2;

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

A5: S_{1}[z]
by A3;

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

S_{1}[v]
by A1;

thus S_{1}[y]
from ABSRED_0:sch 2(A4, A5, A6); :: thesis: verum

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 ; :: 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 A2: x =+=> y ; :: thesis: x ==> y

consider z being Element of X such that

A3: x ==> z and

A4: z =*=> y by A2;

defpred S

A5: S

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

S

thus S