 A1: "\<forall>x\<in> V\<inter>W. \<exists>U\<in>B. x\<in>U \<and> U \<subseteq> V\<inter>W"
  shows "V\<inter>W \<in> {\<Union>A. A\<in>Pow(B)}"
proof
  let?A = "\<Union>x\<in>V\<inter>W. {U\<in>B. x\<in>U \<and> U \<subseteq> V\<inter>W}"
  show "?A\<in>Pow(B)" by auto
  from A1 show "V\<inter>W = \<Union>?A" by blast
qed

text\<open>The next lemma is needed when proving that the would-be topology is
  closed with respect to taking intersections. We show here that intersection
  of two sets from this (would-be) topology can be written as union of sets 
  from the topology.\<close>

lemma Top_1_2_L4:
  assumes A1:  "U\<^sub>1 \<in> {\<Union>A. A\<in>Pow(B)}"   "U\<^sub>2 \<in> {\<Union>A. A\<in>Pow(B)}"
  and A2: "B {satisfies the base condition}"
  shows "\<exists>C. C \<subseteq> {\<Union>A. A\<in>Pow(B)} \<and> U\<^sub>1\<inter>U\<^sub>2 = \<Union>C"
proof -
  from A1 A2 obtain A\<^sub>1 A\<^sub>2 where 
    D1: "A\<^sub>1\<in> Pow(B)"  "U\<^sub>1 = \<Union>A\<^sub>1"  "A\<^sub>2 \<in> Pow(B)"  "U\<^sub>2 = \<Union>A\<^sub>2" 
    by auto
  let?C = "\<Union>U\<in>A\<^sub>1.{U\<inter>V. V\<in>A\<^sub>2}"
  from D1 have "(\<forall>U\<in>A\<^sub>1. U\<in>B) \<and> (\<forall>V\<in>A\<^sub>2. V\<in>B)" by auto
  with A2 have "?C \<subseteq> {\<Union>A. A \<in> Pow(B)}"
    using Top_1_2_L3 SatisfiesBaseCondition_def by auto
  moreover from D1 have "U\<^sub>1 \<inter> U\<^sub>2 = \<Union>?C" by auto
  ultimately show?thesis by auto
qed

text\<open>If $B$ satisfies the base condition, then the collection of unions
  of sets from $B$ is a topology and $B$ is a base for this topology.\<close>

theorem Top_1_2_T1:
  assumes A1: "B {satisfies the base condition}"
  and A2: "T = {\<Union>A. A\<in>Pow(B)}"
  shows "T {is a topology}" and "B {is a base for} T"
proof -
  show "T {is a topology}"
  proof -
    have I: "\<forall>C\<in>Pow(T). \<Union>C \<in> T"
    proof -
      { fix C assume A3: "C \<in> Pow(T)"
        let?Q = "\<Union> {\<Union>{A\<in>Pow(B). U = \<Union>A}. U\<in>C}"
        from A2 A3 have "\<forall>U\<in>C. \<exists>A\<in>Pow(B). U = \<Union>A" by auto
        then have "\<Union>?Q = \<Union>C" using ZF1_1_L10 by simp
        moreover from A2 have "\<Union>?Q \<in> T" by auto
        ultimately have "\<Union>C \<in> T" by simp
      } thus "\<forall>C\<in>Pow(T). \<Union>C \<in> T" by auto
    qed
    moreover have "\<forall>U\<in>T. \<forall> V\<in>T. U\<inter>V \<in> T"
    proof -
      { fix U V assume  "U \<in> T"  "V \<in> T"
        with A1 A2 have "\<exists>C.(C \<subseteq> T \<and> U\<inter>V = \<Union>C)"
        using Top_1_2_L4 by simp
        then obtain C where "C \<subseteq> T" and  "U\<inter>V = \<Union>C"
          by auto
          with I have "U\<inter>V \<in> T" by simp
      } then show "\<forall>U\<in>T. \<forall> V\<in>T. U\<inter>V \<in> T" by simp
    qed
    ultimately show "T {is a topology}" using IsATopology_def
      by simp
  qed
  from A2 have "B\<subseteq>T" by auto
  with A2 show "B {is a base for} T" using IsAbaseFor_def 
    by simp
qed

text\<open>The carrier of the base and topology are the same.\<close>

lemma Top_1_2_L5: assumes "B {is a base for} T"
  shows "\<Union>T = \<Union>B"
  using assms IsAbaseFor_def by auto

text\<open>If $B$ is a base for $T$, then $T$ is the smallest topology containing $B$.
\<close>

lemma base_smallest_top: 
  assumes A1: "B {is a base for} T" and  A2: "S {is a topology}" and A3: "B\<subseteq>S"
  shows "T\<subseteq>S"
proof
  fix U assume "U\<in>T"
  with A1 obtain B\<^sub>U where "B\<^sub>U \<subseteq> B" and "U = \<Union>B\<^sub>U" using IsAbaseFor_def by auto
  with A3 have "B\<^sub>U \<subseteq> S" by auto 
  with A2 \<open>U = \<Union>B\<^sub>U\<close> show "U\<in>S" using IsATopology_def by simp
qed

text\<open>If $B$ is a base for $T$ and $B$ is a topology, then $B=T$.\<close>

lemma base_topology: assumes "B {is a topology}" and "B {is a base for} T"
  shows "B=T" using assms base_sets_open base_smallest_top by blast 

subsection\<open>Product topology\<close>

text\<open>In this section we consider a topology defined on a product of two sets.\<close>

text\<open>Given two topological spaces we can define a topology on the product of 
  the carriers such that the cartesian products of the sets of the topologies 
  are a base for the product topology. Recall that for two collections $S,T$ 
  of sets the product collection is defined (in \<open>ZF1.thy\<close>) as the collections of cartesian 
  products $A\times B$, where $A\in S, B\in T$. The $T\times_tS$ notation is defined as
  an alternative to the verbose  \<open>ProductTopology(T,S)\<close>). \<close>

definition ProductTopology (infixl "\<times>\<^sub>t" 65) where
  "T \<times>\<^sub>t S  \<equiv> {\<Union>W. W \<in> Pow(ProductCollection(T,S))}"

text\<open>The product collection satisfies the base condition.\<close>

lemma Top_1_4_L1: 
  assumes A1: "T {is a topology}"   "S {is a topology}"
  and A2: "A \<in> ProductCollection(T,S)"  "B \<in> ProductCollection(T,S)"
  shows "\<forall>x\<in>(A\<inter>B). \<exists>W\<in>ProductCollection(T,S). (x\<in>W \<and> W \<subseteq> A \<inter> B)"
proof
  fix x assume A3: "x \<in> A\<inter>B"
  from A2 obtain U