constructor 1;
[ apply basic_topology_of_basic_pair
| intros; constructor 1 [ apply continuous_relation_of_relation_pair; ]
| simplify; intro;
]
qed.
constructor 1;
[ apply basic_topology_of_basic_pair
| intros; constructor 1 [ apply continuous_relation_of_relation_pair; ]
| simplify; intro;
]
qed.