∀BP1,BP2.relation_pair BP1 BP2 →
continuous_relation (basic_topology_of_basic_pair BP1) (basic_topology_of_basic_pair BP2).
intros (BP1 BP2 rp);
∀BP1,BP2.relation_pair BP1 BP2 →
continuous_relation (basic_topology_of_basic_pair BP1) (basic_topology_of_basic_pair BP2).
intros (BP1 BP2 rp);