let X be ARS ; :: thesis: ( X is DIAMOND iff the reduction of X is subcommutative )

set R = the reduction of X;

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;

thus ( X is DIAMOND implies the reduction of X is subcommutative ) :: thesis: ( the reduction of X is subcommutative implies X is DIAMOND )

b,c are_convergent<=1_wrt the reduction of X ; :: according to REWRITE1:def 21 :: thesis: X is DIAMOND

let x be Element of X; :: according to ABSRED_0:def 24 :: thesis: for y being Element of X st x <<01>> y holds

x >>01<< y

let y be Element of X; :: thesis: ( x <<01>> y implies x >>01<< y )

given z being Element of X such that A4: ( x <=01= z & z =01=> y ) ; :: according to ABSRED_0:def 22 :: thesis: x >>01<< y

set R = the reduction of X;

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;

thus ( X is DIAMOND implies the reduction of X is subcommutative ) :: thesis: ( the reduction of X is subcommutative implies X is DIAMOND )

proof

assume A3:
for a, b, c being object st [a,b] in the reduction of X & [a,c] in the reduction of X holds
assume A1:
for x, y being Element of X st x <<01>> y holds

x >>01<< y ; :: according to ABSRED_0:def 24 :: thesis: the reduction of X is subcommutative

let a, b, c be object ; :: according to REWRITE1:def 21 :: thesis: ( not [a,b] in the reduction of X or not [a,c] in the reduction of X or b,c are_convergent<=1_wrt the reduction of X )

assume A2: ( [a,b] in the reduction of X & [a,c] in the reduction of X ) ; :: thesis: b,c are_convergent<=1_wrt the reduction of X

then ( a in field the reduction of X & b in field the reduction of X & c in field the reduction of X ) by RELAT_1:15;

then reconsider x = a, y = b, z = c as Element of X by F0;

( x ==> y & x ==> z ) by A2;

then ( x =01=> y & x =01=> z ) ;

then y <<01>> z ;

hence b,c are_convergent<=1_wrt the reduction of X by A1, Ch14; :: thesis: verum

end;x >>01<< y ; :: according to ABSRED_0:def 24 :: thesis: the reduction of X is subcommutative

let a, b, c be object ; :: according to REWRITE1:def 21 :: thesis: ( not [a,b] in the reduction of X or not [a,c] in the reduction of X or b,c are_convergent<=1_wrt the reduction of X )

assume A2: ( [a,b] in the reduction of X & [a,c] in the reduction of X ) ; :: thesis: b,c are_convergent<=1_wrt the reduction of X

then ( a in field the reduction of X & b in field the reduction of X & c in field the reduction of X ) by RELAT_1:15;

then reconsider x = a, y = b, z = c as Element of X by F0;

( x ==> y & x ==> z ) by A2;

then ( x =01=> y & x =01=> z ) ;

then y <<01>> z ;

hence b,c are_convergent<=1_wrt the reduction of X by A1, Ch14; :: thesis: verum

b,c are_convergent<=1_wrt the reduction of X ; :: according to REWRITE1:def 21 :: thesis: X is DIAMOND

let x be Element of X; :: according to ABSRED_0:def 24 :: thesis: for y being Element of X st x <<01>> y holds

x >>01<< y

let y be Element of X; :: thesis: ( x <<01>> y implies x >>01<< y )

given z being Element of X such that A4: ( x <=01= z & z =01=> y ) ; :: according to ABSRED_0:def 22 :: thesis: x >>01<< y