∀ {α : Type u} [t : TopologicalSpace α] {β : Type u_2} [inst : TopologicalSpace β] {B₁ : Set (Set α)}
  {B₂ : Set (Set β)},
  TopologicalSpace.IsTopologicalBasis B₁ →
    TopologicalSpace.IsTopologicalBasis B₂ →
      TopologicalSpace.IsTopologicalBasis (Set.image2 (fun x1 x2 => x1 ×ˢ x2) B₁ B₂)