proposition: Lemma continuous2_cont : forall (D1 D2 D3 :cpo) (f:D1-m> D2 -M-> D3), continuous2 f -> D1 -c> (D2 -C-> D3).
proof: Proof. intros; exists (continuous2_cont_app (f:=f) (continuous2_app H)). red; intros; rewrite continuous2_cont_app_simpl; intro k; simpl. apply Ole_trans with (lub (c:=D2-M->D3) (f@h) k); auto. assert (continuous f); auto. Defined.