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

proof

given z being Element of X such that A1: ( x <=*= z & z =*=> y ) ; :: according to ABSRED_0:def 20 :: thesis: x,y are_divergent_wrt the reduction of X
take z ; :: according to REWRITE1:def 8 :: thesis: ( the reduction of X reduces z,x & the reduction of X reduces z,y )
thus ( the reduction of X reduces z,x & the reduction of X reduces z,y ) by A1; :: 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: ( the reduction of X reduces a,x & the reduction of X reduces a,y ) ; :: according to REWRITE1:def 8 :: thesis: x <<>> y

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

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 20 :: thesis: ( x <=*= z & z =*=> y )
thus ( the reduction of X reduces z,x & the reduction of X reduces z,y ) by A2; :: according to ABSRED_0:def 3 :: thesis: verum

end;

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

then ( a = x & a = y ) by A2, REWRITE1:18;
hence x <<>> y ; :: thesis: verum

end;

end;