let X be ARS ; ( 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 )
( 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
;
ABSRED_0:def 24 the reduction of X is subcommutative
let a,
b,
c be
object ;
REWRITE1:def 21 ( 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 )
;
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;
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
; REWRITE1:def 21 X is DIAMOND
let x be Element of X; ABSRED_0:def 24 for y being Element of X st x <<01>> y holds
x >>01<< y
let y be Element of X; ( x <<01>> y implies x >>01<< y )
given z being Element of X such that A4:
( x <=01= z & z =01=> y )
; ABSRED_0:def 22 x >>01<< y