theorem Lem18: :: ABSRED_0:128

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