let A be non empty Preorder; :: thesis: for x, y being Element of A st x <= y holds
(proj A) . x <= (proj A) . y
let x, y be Element of A; :: thesis: ( x <= y implies (proj A) . x <= (proj A) . y )
assume A1: x <= y ; :: thesis: (proj A) . x <= (proj A) . y
reconsider X = Class ((EqRelOf A),x) as Element of Class (EqRelOf A) by EQREL_1:def 3;
reconsider Y = Class ((EqRelOf A),y) as Element of Class (EqRelOf A) by EQREL_1:def 3;
A2: [X,Y] in the InternalRel of (QuotientOrder A) by A1, Def7;
( X = (proj A) . x & Y = (proj A) . y ) by Def8;
hence (proj A) . x <= (proj A) . y by A2, ORDERS_2:def 5; :: thesis: verum