theorem Lem1: :: ABSRED_0:9

for X being ARS
for x, y being Element of X st x =01=> y holds
x =*=> y by Th2;