+*)
+
+include "o-basic_pairs.ma".
+(* Qui, per fare le cose per bene, ci serve la nozione di funtore categorico *)
+definition o_basic_pair_of_basic_pair: cic:/matita/formal_topology/basic_pairs/basic_pair.ind#xpointer(1/1) → basic_pair.
+ intro;
+ constructor 1;
+ [ apply (SUBSETS (concr b));
+ | apply (SUBSETS (form b));
+ | apply (orelation_of_relation ?? (rel b)); ]
+qed.
+
+definition o_relation_pair_of_relation_pair:
+ ∀BP1,BP2.cic:/matita/formal_topology/basic_pairs/relation_pair.ind#xpointer(1/1) BP1 BP2 →
+ relation_pair (o_basic_pair_of_basic_pair BP1) (o_basic_pair_of_basic_pair BP2).
+ intros;
+ constructor 1;
+ [ apply (orelation_of_relation ?? (r \sub \c));
+ | apply (orelation_of_relation ?? (r \sub \f));
+ |
+ ]
+qed.
\ No newline at end of file