proposition: Lemma subspace_basis (B : Family X) : open_basis B -> open_basis (Im B (inverse_image subspace_inc)).
proof: Proof. intros. constructor. - intros. inversion H0; subst; clear H0. apply subspace_inc_continuous. apply H. assumption. - intros. rewrite subspace_open_char in H0. destruct H0 as [V []]. subst. pose proof (open_basis_cover B H (proj1_sig x) V H0). destruct H2 as [V0 [? []]]. { destruct H1. assumption. } exists (inverse_image subspace_inc V0). repeat split. + eexists V0; auto. + apply H3. apply H5. + apply H4. Qed.
imports: ZornsLemma(CardinalsEns DecidableDec FiniteIntersections Proj1SigInjective) Topology(WeakTopology)