record continuous_relation (S,T: basic_topology) : Type1 ≝
{ cont_rel:> arrows1 ? S T;
reduced: ∀U. U = J ? U → image ?? cont_rel U = J ? (image ?? cont_rel U);
saturated: ∀U. U = A ? U → minus_star_image ?? cont_rel U = A ? (minus_star_image ?? cont_rel U)
}.
record continuous_relation (S,T: basic_topology) : Type1 ≝
{ cont_rel:> arrows1 ? S T;
reduced: ∀U. U = J ? U → image ?? cont_rel U = J ? (image ?? cont_rel U);
saturated: ∀U. U = A ? U → minus_star_image ?? cont_rel U = A ? (minus_star_image ?? cont_rel U)
}.