theorem Lem17: :: ABSRED_0:139

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