:: deftheorem Def9 defines -respecting FOMODEL3:def 9 :
for E, F being Relation
for f being Function holds
( f is E,F -respecting iff for x1, x2 being set st [x1,x2] in E holds
[(f . x1),(f . x2)] in F );