:: deftheorem respadd defines respecting_addition REALALG1:def 3 :
for L being addLoopStr
for R being Relation of L holds
( R is respecting_addition iff for a, b, c being Element of L st a <=_ R,b holds
a + c <=_ R,b + c );