proposition: Lemma continuous_sym : forall (D1 D2:cpo) (F : D1-m> D1 -M-> D2), (forall x y, F x y == F y x) -> (forall k:D1, continuous (F k)) -> continuous F.
proof: Proof. red; intros; intro k. apply Ole_trans with (F k (lub h)); auto. apply Ole_trans with (lub ((F k) @ h)); auto. Qed.