Outdated comment out of filterSpair lemma?

[affeldt-aist]

analysis/theories/topology.v

Lines 1527 to 1536 in 3f7d5f0

	(* Lemma filterSpair (T T' : Type) (F : set (set T)) (F' : set (set T')) : *)
	(* Filter F -> Filter F' -> *)
	(* forall (P : set T) (P' : set T') (Q : set (T * T')), *)
	(* (forall x x', P x -> P' x' -> Q (x, x')) -> F P /\ F' P' -> *)
	(* filter_prod F F' Q. *)
	(* Proof. *)
	(* move=> FF FF' P P' Q PQ [FP FP']; near=> x. *)
	(* have := PQ x.1 x.2; rewrite -surjective_pairing; apply; near: x; *)
	(* by [apply: cvg_fst|apply: cvg_snd]. *)
	(* Grab Existential Variables. all: end_near. Qed. *)

This lemma can actually by uncommented and it type-checks but it is of course not used.