proposition: Lemma prl_ne2_sigma_maximal_ne A: (forall i, inc i (psI S) -> prl_ne1_condii' i) -> pr1_ne2_hyp3_weak -> maximal prl_ne2_sigma_order A -> nonempty (projective_limit S).
proof: Proof. move => ha hb hc. move: (proj2 (prl_ne2_sigma_maximal_prop3 ha hb hc)) => xx; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)