theorem LemZ: :: ABSRED_0:82

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