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₁[ Element of X] means $1 ==> z;
C: for u, v being Element of X st u ==> v & S₁[u] holds
S₁[v] by A;
D: for u, v being Element of X st u =*=> v & S₁[u] holds
S₁[v] from ABSRED_0:sch 1(C);
thus y ==> z by B, D; :: thesis: verum