let X be ARS ; 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; ( ( 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
; for x, y being Element of X st x ==> z & x =*=> y holds
y ==> z
let x, y be Element of X; ( x ==> z & x =*=> y implies y ==> z )
assume B:
( x ==> z & x =*=> y )
; y ==> z
defpred S1[ Element of X] means $1 ==> z;
C:
for u, v being Element of X st u ==> v & S1[u] holds
S1[v]
by A;
D:
for u, v being Element of X st u =*=> v & S1[u] holds
S1[v]
from ABSRED_0:sch 1(C);
thus
y ==> z
by B, D; verum