let X be ARS ; :: thesis: for x, y being Element of X holds
( x <<01>> y iff x,y are_divergent<=1_wrt the reduction of X )
let x, y be Element of X; :: thesis: ( x <<01>> y iff x,y are_divergent<=1_wrt the reduction of X )
set R = the reduction of X;
thus ( x <<01>> y implies x,y are_divergent<=1_wrt the reduction of X ) :: thesis: ( x,y are_divergent<=1_wrt the reduction of X implies x <<01>> y )

proof

given z being Element of X such that A1: ( x <=01= z & z =01=> y ) ; :: according to ABSRED_0:def 22 :: thesis: x,y are_divergent<=1_wrt the reduction of X
take z ; :: according to REWRITE1:def 10 :: thesis: ( ( [z,x] in the reduction of X or x = z ) & ( [z,y] in the reduction of X or y = z ) )
( ( z ==> x or z = x ) & ( z ==> y or z = y ) ) by A1;
hence ( ( [z,x] in the reduction of X or z = x ) & ( [z,y] in the reduction of X or z = y ) ) ; :: thesis: verum

end;

set A = the carrier of X;
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: ( ( [a,x] in the reduction of X or a = x ) & ( [a,y] in the reduction of X or a = y ) ) ; :: according to REWRITE1:def 10 :: 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 22 :: thesis: ( x <=01= z & z =01=> y )
thus ( z = x or z ==> x ) by A2; :: according to ABSRED_0:def 2 :: thesis: z =01=> y
thus ( z = y or z ==> y ) by A2; :: according to ABSRED_0:def 2 :: thesis: verum