proposition: Lemma opredU : join_closed S.
proof: Proof. by move=> x y xS yS; rewrite -set_join2 opredSJ// => _ [] ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(ssrnat bigop classical_sets)