Let X, Tx, Y and Ty be given.
Assume HTx: topology_on X Tx.
Assume HTy: topology_on Y Ty.
We will prove ∃S : set, S = product_subbasis X Tx Y Ty ∧ generated_topology (setprod X Y) S = product_topology X Tx Y Ty.
We use (product_subbasis X Tx Y Ty) to witness the existential quantifier.
We will prove product_subbasis X Tx Y Ty = product_subbasis X Tx Y Ty ∧ generated_topology (setprod X Y) (product_subbasis X Tx Y Ty) = product_topology X Tx Y Ty.
Apply andI to the current goal.
Use reflexivity.
Use reflexivity.
∎