include "o-basic_pairs_to_o-basic_topologies.ma".
lemma rOR_full :
- ∀rS,rT:rOBP.∀f:arrows2 BTop (OR (ℱ_2 rS)) (OR (ℱ_2 rT)).
- exT22 ? (λg:arrows2 rOBP rS rT.
+ ∀s,t:rOBP.∀f:arrows2 OBTop (OR (ℱ_2 s)) (OR (ℱ_2 t)).
+ exT22 ? (λg:arrows2 rOBP s t.
map_arrows2 ?? OR ?? (ℳ_2 g) = f).
-intros; cases f (c H1 H2); simplify;
+intros; cases f (h H1 H2); clear f; simplify;
+change in ⊢ (? ? (λg:?.? ? ? (? ? ? %) ?)) with
+ (o_continuous_relation_of_o_relation_pair ?? (ℳ_2 g)).
+
STOP;