definition downarrow: ∀S:BTop. unary_morphism (Ω \sup S) (Ω \sup S).
intros; constructor 1;
[ apply (λU:Ω \sup S.{a | ∃b:carrbt S. b ∈ U ∧ a ∈ A ? (singleton ? b)});
definition downarrow: ∀S:BTop. unary_morphism (Ω \sup S) (Ω \sup S).
intros; constructor 1;
[ apply (λU:Ω \sup S.{a | ∃b:carrbt S. b ∈ U ∧ a ∈ A ? (singleton ? b)});