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

(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