Closed sets are elegantly described using coreflexives and inclusion
EndoRelation A R\textbf{EndoRelation} \; A \; REndoRelationAR
PowerSet A X\textbf{PowerSet} \; A \; XPowerSetAX
ΦX;R⊆R;ΦX\Phi_X ; R \subseteq R ; \Phi_XΦX;R⊆R;ΦX
pred Closed(A: set univ, R: univ->univ, X: set univ) { EndoRelation[A,R] X in A X<:R in R:>X }
Last updated 1 year ago