definition continuous_relation_setoid: basic_topology → basic_topology → setoid1.
intros (S T); constructor 1;
[ apply (continuous_relation S T)
| constructor 1;
[ apply (λr,s:continuous_relation S T.∀b. A ? (ext ?? r b) = A ? (ext ?? s b));
| simplify; intros; apply refl1;
definition continuous_relation_setoid: basic_topology → basic_topology → setoid1.
intros (S T); constructor 1;
[ apply (continuous_relation S T)
| constructor 1;
[ apply (λr,s:continuous_relation S T.∀b. A ? (ext ?? r b) = A ? (ext ?? s b));
| simplify; intros; apply refl1;