Conditional order induced by a lift

For every small type $E$ and every reading $r:E\to\mathbb R$, define $e\prec_r f$ to mean exactly $r(e)<r(f)$. The theorem asserts the conjunction that: for every $E,r$, no event precedes itself and, for every $e,f,g\in E$, $e\prec_r f$ together with $f\prec_r g$ implies $e\prec_r g$; for every $E,r$, if $r$ is injective, then every distinct $e,f\in E$ satisfy $e\prec_r f$ or $f\prec_r e$; for every $E$ equipped with a LinearOrder and every $r$ strictly monotone for that order, $e\prec_r f\iff e<f$ for every $e,f$; and there exists at least one reading $r:\operatorname{Fin}3\to\mathbb R$ such that $r(0)=0$, $r(1)=4\pi$, $r(2)=2\pi$, $r(2)-r(0)=2\pi$, and $r$ is not strictly monotone for the canonical order on $\operatorname{Fin}3$. No nonemptiness hypothesis is imposed in the universal clauses, so they also cover the empty event type vacuously; the existential clause specifies existence but not uniqueness of the reading.