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 )
proof
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 ; :: thesis: verum
end;
assume A3: for a, b, c being object st [a,b] in the reduction of X & [a,c] in the reduction of X holds
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
per cases ( ( x <== z & z ==> y ) or ( x = z & z = y ) or ( x <== z & z = y ) or ( x = z & z ==> y ) ) by A4;
suppose ( x <== z & z ==> y ) ; :: thesis: x >>01<< y
hence x >>01<< y by ; :: thesis: verum
end;
suppose ( x = z & z = y ) ; :: thesis: x >>01<< y
hence x >>01<< y ; :: thesis: verum
end;
suppose ( x <== z & z = y ) ; :: thesis: x >>01<< y
hence x >>01<< y by Th17; :: thesis: verum
end;
suppose ( x = z & z ==> y ) ; :: thesis: x >>01<< y
hence x >>01<< y by Th17; :: thesis: verum
end;
end;