theorem nhdsGT_basis_Ioc {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMaxOrder α] (a : α) : (nhdsWithin a (Set.Ioi a)).HasBasis (fun (x : α) => a < x) (Set.Ioc a)