theorem Th17a: :: ABSRED_0:138

for X being ARS
for x, y being Element of X st x ==> y holds
x >><< y by Th17, Lem18a;