theorem Lem1A: :: ABSRED_0:36

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