:: deftheorem defines midpoints-preserving MAZURULM:def 3 :
for E, F being non empty RLSStruct
for f being Function of E,F holds
( f is midpoints-preserving iff for a, b being Point of E holds f . ((1 / 2) * (a + b)) = (1 / 2) * ((f . a) + (f . b)) );