proposition: Lemma ordinal_setI x: nonempty x -> ordinal_set x -> inc (intersection x) x.
proof: Proof. move=> nex alo; ex_middle nix. have [tic dix]: (trans_dec_set (intersection x)). apply: trans_dec_setI => y yx; exact: (ordinal_trans_dec (alo _ yx)). case:(irreflexive_decent dix). apply: (setI_i nex)=> a ax; apply: (alo _ ax _ (setI_s1 ax) tic); dneg xx; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)