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 S1[ 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 & S1[y] holds
S1[z]
proof
let y, z be Element of X; :: thesis: ( y ==> z & S1[y] implies S1[z] )
assume A3: y ==> z ; :: thesis: ( not S1[y] or S1[z] )
given u being Element of X such that A4: ( x =*=> u & u ==> y ) ; :: thesis: S1[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 & S1[y] holds
S1[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 S1[ 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 & S1[z] holds
S1[y]
proof
let x, z be Element of X; :: thesis: ( x ==> z & S1[z] implies S1[x] )
assume A3: x ==> z ; :: thesis: ( not S1[z] or S1[x] )
given u being Element of X such that A4: ( z ==> u & u =*=> y ) ; :: thesis: S1[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 & S1[z] holds
S1[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