:: deftheorem Def8 defines proj ORDERS_5:def 8 :
for A being Preorder
for b₂ being Function of A,(QuotientOrder A) holds
( b₂ = proj A iff for x being Element of A holds b₂ . x = Class ((EqRelOf A),x) );