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