theorem Th2: :: ABSRED_0:2

for X being ARS
for x, y being Element of X st x ==> y holds
x =*=> y by REWRITE1:15;