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

y ==> z ) holds

for x, y being Element of X st x ==> z & x =*=> y holds

y ==> z

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

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

y ==> z )

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

y ==> z ; :: thesis: for x, y being Element of X st x ==> z & x =*=> y holds

y ==> z

let x, y be Element of X; :: thesis: ( x ==> z & x =*=> y implies y ==> z )

assume B: ( x ==> z & x =*=> y ) ; :: thesis: y ==> z

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

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

S_{1}[v]
by A;

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

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

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

y ==> z ) holds

for x, y being Element of X st x ==> z & x =*=> y holds

y ==> z

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

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

y ==> z )

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

y ==> z ; :: thesis: for x, y being Element of X st x ==> z & x =*=> y holds

y ==> z

let x, y be Element of X; :: thesis: ( x ==> z & x =*=> y implies y ==> z )

assume B: ( x ==> z & x =*=> y ) ; :: thesis: y ==> z

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 y ==> z by B, D; :: thesis: verum