proposition: Lemma opredSJ (B : set U) : set_join (val @` B) \in S.
proof: Proof. by apply: opredSJ => _ [y By] <- /=; apply: valP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(ssrnat bigop classical_sets)