:: deftheorem Def12 defines eqSupport ORDERS_5:def 12 :
for A being Preorder
for X being Element of (QuotientOrder A)
for f being Function
for b₄ being Subset of A holds
( b₄ = eqSupport (f,X) iff ex D being a_partition of the carrier of A ex Y being Element of D st
( D = the carrier of (QuotientOrder A) & Y = X & b₄ = eqSupport (f,Y) ) );