Description: Subset implication for an indexed intersection. (Contributed by Glauco Siliprandi, 23-Oct-2021)