:: deftheorem defines eqSupport ORDERS_5:def 13 :
for A being Preorder
for X being Element of (QuotientOrder A)
for f being Function holds eqSupport (f,X) = (support f) /\ X;