Upper Set

$\textbf{UpperSet} \; A \; R \; X$

---

$\textbf{Preorder} \; A \; R$

$\textbf{Closed} \; A \; R \; X$

---

pred UpperSet(A: set univ, R: univ->univ, X: set univ) {
  Preorder[A,R]
  Closed[A,R,X]
}

$\textbf{AtMost} \; B \; R \; U \; H$

---

$\textbf{UpperSet} \; B \; R \; U$

$\textbf{UpperSet} \; B \; R \; H$

$\textbf{Includes} \; U \; H$

---

pred AtMost(B: set univ, R: univ -> univ, U: set univ, H: set univ) {
  UpperSet[B,R,U]
  UpperSet[B,R,H]
  U in H
}