theorem LemB: :: ABSRED_0:38

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