for X being ARS
for x, y, z being Element of X st X is DIAMOND & x <=01= y & y =*=> z holds
ex u being Element of X st
( x =*=> u & u <=01= z )