:: deftheorem Def7 defines QuotientOrder ORDERS_5:def 7 :
for A being Preorder
for b₂ being strict RelStr holds
( b₂ = QuotientOrder A iff ( the carrier of b₂ = Class (EqRelOf A) & ( for X, Y being Element of Class (EqRelOf A) holds
( [X,Y] in the InternalRel of b₂ iff ex x, y being Element of A st
( X = Class ((EqRelOf A),x) & Y = Class ((EqRelOf A),y) & x <= y ) ) ) ) );