constructor 1;
[ apply o_basic_topology_of_o_basic_pair;
| intros; constructor 1;
[ apply o_continuous_relation_of_o_relation_pair;
| apply hide;
intros; whd; unfold o_continuous_relation_of_o_relation_pair; simplify;;
constructor 1;
[ apply o_basic_topology_of_o_basic_pair;
| intros; constructor 1;
[ apply o_continuous_relation_of_o_relation_pair;
| apply hide;
intros; whd; unfold o_continuous_relation_of_o_relation_pair; simplify;;