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

( x >>01<< y iff x,y are_convergent<=1_wrt the reduction of X )

let x, y be Element of X; :: thesis: ( x >>01<< y iff x,y are_convergent<=1_wrt the reduction of X )

set R = the reduction of X;

thus ( x >>01<< y implies x,y are_convergent<=1_wrt the reduction of X ) :: thesis: ( x,y are_convergent<=1_wrt the reduction of X implies x >>01<< 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: ( ( [x,a] in the reduction of X or x = a ) & ( [y,a] in the reduction of X or y = a ) ) ; :: according to REWRITE1:def 9 :: thesis: x >>01<< y

( a in field the reduction of X or a = x or a = y ) by A2, RELAT_1:15;

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

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

thus ( x = z or x ==> z ) by A2; :: according to ABSRED_0:def 2 :: thesis: z <=01= y

thus ( y = z or y ==> z ) by A2; :: according to ABSRED_0:def 2 :: thesis: verum

( x >>01<< y iff x,y are_convergent<=1_wrt the reduction of X )

let x, y be Element of X; :: thesis: ( x >>01<< y iff x,y are_convergent<=1_wrt the reduction of X )

set R = the reduction of X;

thus ( x >>01<< y implies x,y are_convergent<=1_wrt the reduction of X ) :: thesis: ( x,y are_convergent<=1_wrt the reduction of X implies x >>01<< y )

proof

set A = the carrier of X;
given z being Element of X such that A1:
( z <=01= x & y =01=> z )
; :: according to ABSRED_0:def 23 :: thesis: x,y are_convergent<=1_wrt the reduction of X

take z ; :: according to REWRITE1:def 9 :: thesis: ( ( [x,z] in the reduction of X or x = z ) & ( [y,z] in the reduction of X or y = z ) )

( ( x ==> z or z = x ) & ( y ==> z or z = y ) ) by A1;

hence ( ( [x,z] in the reduction of X or x = z ) & ( [y,z] in the reduction of X or y = z ) ) ; :: thesis: verum

end;take z ; :: according to REWRITE1:def 9 :: thesis: ( ( [x,z] in the reduction of X or x = z ) & ( [y,z] in the reduction of X or y = z ) )

( ( x ==> z or z = x ) & ( y ==> z or z = y ) ) by A1;

hence ( ( [x,z] in the reduction of X or x = z ) & ( [y,z] in the reduction of X or y = z ) ) ; :: 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: ( ( [x,a] in the reduction of X or x = a ) & ( [y,a] in the reduction of X or y = a ) ) ; :: according to REWRITE1:def 9 :: thesis: x >>01<< y

( a in field the reduction of X or a = x or a = y ) by A2, RELAT_1:15;

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

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

thus ( x = z or x ==> z ) by A2; :: according to ABSRED_0:def 2 :: thesis: z <=01= y

thus ( y = z or y ==> z ) by A2; :: according to ABSRED_0:def 2 :: thesis: verum