proposition: Lemma OS_sup E: ordinal_set E -> ordinalp (\osup E).
proof: Proof. move=> alo; apply: ordinal_pr. by apply: transitive_setU => y yx; apply: ordinal_transitive; apply: alo. move=> y /setU_P [a ya ax]. exact: (Os_ordinal (alo _ ax) ya). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)