proposition: Lemma bridges_lemma1a : l_u_b OF P.
proof: Proof. apply (lubp P P_is_inhabited). case is_finite_P. intro N. intros. case s. intro r. intro. exists (saghf r N). red in |- *. intros x H z H0. apply less_transitive_unfolded with (y := x). assumption. case (s0 x H). intro m. intros H1 H2. apply less_wdl with (x := r m). apply Psaghf. assumption. assumption. intros. cut ((forall k : nat, k <= card -> seq k[<]y) or {j : nat | P (seq j) | x[<]seq j}). intro H0. case H0. intro c. left. red in |- *. intros x0 H1 z H2. apply less_transitive_unfolded with (y := x0). assumption. elim (Pindeks x0 H1). intros. apply less_wdl with (x := seq (indeks x0 H1)). apply c. assumption. assumption. intro e. right. case e. intro j. intros H2 H3. exists (seq j). assumption. assumption. case (bounded_quantifier_informative card) with (phi := fun k : nat => seq k[<]y) (psi := fun k : nat => x[<]seq k). intros. cut (x[<]seq m or seq m[<]y). intro H1. case H1. intro. right. assumption. intro. left. assumption. apply less_cotransitive_unfolded. assumption. intros. left. assumption. intro e. right. case e. intro j. intros. exists j. apply is_onto_seq_P. apply Cle_to. assumption. assumption. Qed.
imports: CoRN.reals.Bridges_LUB