qed.
definition o_continuous_relation_of_o_relation_pair:
- ∀BP1,BP2.arrows2 OBP BP1 BP2 →
- arrows2 OBTop (o_basic_topology_of_o_basic_pair BP1) (o_basic_topology_of_o_basic_pair BP2).
+ ∀BP1,BP2.BP1 ⇒_\obp2 BP2 →
+ (o_basic_topology_of_o_basic_pair BP1) ⇒_\obt2 (o_basic_topology_of_o_basic_pair BP2).
intros (BP1 BP2 t);
constructor 1;
[ apply (t \sub \f);
qed.
-definition OR : carr3 (arrows3 CAT2 OBP OBTop).
+definition OR : carr3 (OBP ⇒_\c3 OBTop).
constructor 1;
[ apply o_basic_topology_of_o_basic_pair;
| intros; constructor 1;