Description: Alternate definition of the class of disjoints (via quotient-map
stability). Disjs is the class of relations r whose quotient-map
QMap r is again disjoint and whose induced quotient-carrier is
element-disjoint. This is the definitional "stability-by-decomposition"
packaging of disjointness: it builds Disjs from two internal layers
(i) a carrier-layer constraint and (ii) a map-layer closure constraint.
This is deliberately different from "u R x" style definitions: it makes
the carrier of blocks and the uniqueness-of-representatives discipline
first-class and reusable (via QMap ) rather than implicit.
(Contributed by Peter Mazsa, 16-Feb-2026)