We will prove Lindelof_space ordered_square ordered_square_topology ∧ ¬ Lindelof_space ordered_square_open_strip ordered_square_subspace_topology.

Apply andI to the current goal.

An exact proof term for the current goal is ordered_square_Lindelof.

An exact proof term for the current goal is ordered_square_open_strip_not_Lindelof.

∎