let X be ARS ; :: thesis: for x, y being Element of X holds
( x =+=> y iff ex z being Element of X st
( x =*=> z & z ==> y ) )
let x, y be Element of X; :: thesis: ( x =+=> y iff ex z being Element of X st
( x =*=> z & z ==> y ) )
thus ( x =+=> y implies ex z being Element of X st
( x =*=> z & z ==> y ) ) :: thesis: ( ex z being Element of X st
( x =*=> z & z ==> y ) implies x =+=> y )

proof

given z being Element of X such that A1: ( x ==> z & z =*=> y ) ; :: according to ABSRED_0:def 4 :: thesis: ex z being Element of X st
( x =*=> z & z ==> y )
defpred S₁[ Element of X] means ex u being Element of X st
( x =*=> u & u ==> $1 );
A2: for y, z being Element of X st y ==> z & S₁[y] holds
S₁[z]

proof

let y, z be Element of X; :: thesis: ( y ==> z & S₁[y] implies S₁[z] )
assume A3: y ==> z ; :: thesis: ( not S₁[y] or S₁[z] )
given u being Element of X such that A4: ( x =*=> u & u ==> y ) ; :: thesis: S₁[z]
take y ; :: thesis: ( x =*=> y & y ==> z )
u =*=> y by A4, Th2;
hence ( x =*=> y & y ==> z ) by A3, A4, Th3; :: thesis: verum

end;

A5: for y, z being Element of X st y =*=> z & S₁[y] holds
S₁[z] from ABSRED_0:sch 1(A2);
thus ex z being Element of X st
( x =*=> z & z ==> y ) by A1, A5; :: thesis: verum

end;

given z being Element of X such that A6: ( x =*=> z & z ==> y ) ; :: thesis: x =+=> y
defpred S₁[ Element of X] means ex u being Element of X st
( $1 ==> u & u =*=> y );
A2: for y, z being Element of X st y ==> z & S₁[z] holds
S₁[y]

proof

let x, z be Element of X; :: thesis: ( x ==> z & S₁[z] implies S₁[x] )
assume A3: x ==> z ; :: thesis: ( not S₁[z] or S₁[x] )
given u being Element of X such that A4: ( z ==> u & u =*=> y ) ; :: thesis: S₁[x]
take z ; :: thesis: ( x ==> z & z =*=> y )
z =*=> u by A4, Th2;
hence ( x ==> z & z =*=> y ) by A3, A4, Th3; :: thesis: verum

end;

A5: for y, z being Element of X st y =*=> z & S₁[z] holds
S₁[y] from ABSRED_0:sch 3(A2);
thus ex z being Element of X st
( x ==> z & z =*=> y ) by A5, A6; :: according to ABSRED_0:def 4 :: thesis: verum