Closed

Closed sets are elegantly described using coreflexives and inclusion

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

---

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

$\textbf{PowerSet} \; A \; X$

$\Phi_X ; R \subseteq R ; \Phi_X$

---

pred Closed(A: set univ, R: univ->univ, X: set univ) {
  EndoRelation[A,R]
  X in A
  X<:R in R:>X
}