proposition: Lemma subspace_subbasis (B : Family X) : subbasis B -> subbasis (Im B (fun Bx => inverse_image subspace_inc Bx)).
proof: Proof. intros. constructor. - intros. inversion H0; subst; clear H0. apply subspace_inc_continuous. apply subbasis_elements in H1; assumption. - intros U x HUx HU. rewrite subspace_open_char in HU. destruct HU as [V [HV HUV]]. subst. inversion HUx; subst; clear HUx. apply subbasis_cover with (SB := B) (x := subspace_inc x) in HV as [W [HWx [HWfin HWV]]]; auto. exists (inverse_image subspace_inc W); repeat split; auto. + apply finite_intersections_Im_inverse_image. assumption. + destruct H1. auto. Qed.
imports: ZornsLemma(CardinalsEns DecidableDec FiniteIntersections Proj1SigInjective) Topology(WeakTopology)