Let X and Tx be given.
Assume Hscc: second_countable_space X Tx.
We will prove Lindelof_space X Tx.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (andEL (topology_on X Tx) (∃B : set, basis_on X B ∧ countable_set B ∧ basis_generates X B Tx) Hscc).
We will prove topology_on X Tx ∧ ∀U : set, open_cover X Tx U → ∃V : set, countable_subcollection V U ∧ covers X V.
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
Let U be given.
Assume HU: open_cover X Tx U.
An exact proof term for the current goal is (countable_basis_implies_Lindelof X Tx HTx Hscc U HU).
∎