let A be 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
then A2: [x,y] in EqRelOf A by Def6;
A3: ( x in the carrier of A & y in the carrier of A ) by A1, Th29;
thus (proj A) . x = Class ((EqRelOf A),x) by Def8
.= Class ((EqRelOf A),y) by A2, A3, EQREL_1:35
.= (proj A) . y by Def8 ; :: thesis: verum