theorem Lem2: :: ABSRED_0:10

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