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₁[ Element of X] means x ==> $1;
A5: S₁[z] by A3;
A6: for u, v being Element of X st u ==> v & S₁[u] holds
S₁[v] by A1;
thus S₁[y] from ABSRED_0:sch 2(A4, A5, A6); :: thesis: verum