theorem Lem43: :: ABSRED_0:70

for X being ARS
for x, y being Element of X st ( x <=01= y or x ==> y ) holds
x <=01=> y