:: deftheorem respmult defines respecting_multiplication REALALG1:def 4 :
for L being multLoopStr_0
for R being Relation of L holds
( R is respecting_multiplication iff for a, b, c being Element of L st a <=_ R,b & 0. L <=_ R,c holds
a * c <=_ R,b * c );