theorem :: ABSRED_0:150

for X being ARS holds
( X is DIAMOND iff the reduction of X is subcommutative )