theorem :: ORDERS_5:37

for A being Preorder
for x, y being Element of A st x =~ y holds
(proj A) . x = (proj A) . y