theorem Lem19: :: ABSRED_0:148

for X being ARS
for x, y being Element of X st x <<>> y holds
x <=*=> y