Proposition. For every set and preorder on , exists a set and function such that iff
Proof. Take . For , let denote the set of values with . Note that is of type , as promised. I claim that :
Take and . Then so by transitivity so . Thus .
Take . Note so so so .