∀P,Q. arrows2 OBTop P Q → Ocontinuous_relation_setoid P Q ≝ λP,Q,x.x.
coercion Ocontinuous_relation_setoid_of_arrows2_OBTop.
+notation > "B ⇒_\obt2 C" right associative with precedence 72 for @{'arrows2_OBT $B $C}.
+notation "B ⇒\sub (\obt 2) C" right associative with precedence 72 for @{'arrows2_OBT $B $C}.
+interpretation "'arrows2_OBT" 'arrows2_OBT A B = (arrows2 OBTop A B).
+
+
(*
(*CSC: unused! *)
(* this proof is more logic-oriented than set/lattice oriented *)