let X be ARS ; :: thesis: for x, y being Element of X holds

( x >><< y iff x,y are_convergent_wrt the reduction of X )

let x, y be Element of X; :: thesis: ( x >><< y iff x,y are_convergent_wrt the reduction of X )

set R = the reduction of X;

thus ( x >><< y implies x,y are_convergent_wrt the reduction of X ) :: thesis: ( x,y are_convergent_wrt the reduction of X implies x >><< y )

F0: field the reduction of X c= the carrier of X \/ the carrier of X by RELSET_1:8;

given a being object such that A2: ( the reduction of X reduces x,a & the reduction of X reduces y,a ) ; :: according to REWRITE1:def 7 :: thesis: x >><< y

( x >><< y iff x,y are_convergent_wrt the reduction of X )

let x, y be Element of X; :: thesis: ( x >><< y iff x,y are_convergent_wrt the reduction of X )

set R = the reduction of X;

thus ( x >><< y implies x,y are_convergent_wrt the reduction of X ) :: thesis: ( x,y are_convergent_wrt the reduction of X implies x >><< y )

proof

set A = the carrier of X;
given z being Element of X such that A1:
( z <=*= x & y =*=> z )
; :: according to ABSRED_0:def 21 :: thesis: x,y are_convergent_wrt the reduction of X

take z ; :: according to REWRITE1:def 7 :: thesis: ( the reduction of X reduces x,z & the reduction of X reduces y,z )

thus ( the reduction of X reduces x,z & the reduction of X reduces y,z ) by A1; :: thesis: verum

end;take z ; :: according to REWRITE1:def 7 :: thesis: ( the reduction of X reduces x,z & the reduction of X reduces y,z )

thus ( the reduction of X reduces x,z & the reduction of X reduces y,z ) by A1; :: thesis: verum

F0: field the reduction of X c= the carrier of X \/ the carrier of X by RELSET_1:8;

given a being object such that A2: ( the reduction of X reduces x,a & the reduction of X reduces y,a ) ; :: according to REWRITE1:def 7 :: thesis: x >><< y

per cases
( a in field the reduction of X or not a in field the reduction of X )
;

end;

suppose
a in field the reduction of X
; :: thesis: x >><< y

then reconsider z = a as Element of X by F0;

take z ; :: according to ABSRED_0:def 21 :: thesis: ( x =*=> z & z <=*= y )

thus ( the reduction of X reduces x,z & the reduction of X reduces y,z ) by A2; :: according to ABSRED_0:def 3 :: thesis: verum

end;take z ; :: according to ABSRED_0:def 21 :: thesis: ( x =*=> z & z <=*= y )

thus ( the reduction of X reduces x,z & the reduction of X reduces y,z ) by A2; :: according to ABSRED_0:def 3 :: thesis: verum