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 )

defpred S_{1}[ 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_{1}[z] holds

S_{1}[y]
_{1}[z] holds

S_{1}[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

( 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 A6:
( x =*=> z & z ==> y )
; :: thesis: x =+=> y
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_{1}[ 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_{1}[y] holds

S_{1}[z]
_{1}[y] holds

S_{1}[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;( x =*=> z & z ==> y )

defpred S

( x =*=> u & u ==> $1 );

A2: for y, z being Element of X st y ==> z & S

S

proof

A5:
for y, z being Element of X st y =*=> z & S
let y, z be Element of X; :: thesis: ( y ==> z & S_{1}[y] implies S_{1}[z] )

assume A3: y ==> z ; :: thesis: ( not S_{1}[y] or S_{1}[z] )

given u being Element of X such that A4: ( x =*=> u & u ==> y ) ; :: thesis: S_{1}[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;assume A3: y ==> z ; :: thesis: ( not S

given u being Element of X such that A4: ( x =*=> u & u ==> y ) ; :: thesis: S

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

u =*=> y by A4, Th2;

hence ( x =*=> y & y ==> z ) by A3, A4, Th3; :: thesis: verum

S

thus ex z being Element of X st

( x =*=> z & z ==> y ) by A1, A5; :: thesis: verum

defpred S

( $1 ==> u & u =*=> y );

A2: for y, z being Element of X st y ==> z & S

S

proof

A5:
for y, z being Element of X st y =*=> z & S
let x, z be Element of X; :: thesis: ( x ==> z & S_{1}[z] implies S_{1}[x] )

assume A3: x ==> z ; :: thesis: ( not S_{1}[z] or S_{1}[x] )

given u being Element of X such that A4: ( z ==> u & u =*=> y ) ; :: thesis: S_{1}[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;assume A3: x ==> z ; :: thesis: ( not S

given u being Element of X such that A4: ( z ==> u & u =*=> y ) ; :: thesis: S

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

z =*=> u by A4, Th2;

hence ( x ==> z & z =*=> y ) by A3, A4, Th3; :: thesis: verum

S

thus ex z being Element of X st

( x ==> z & z =*=> y ) by A5, A6; :: according to ABSRED_0:def 4 :: thesis: verum