for I, G being set
for sf being Subset-Family of I st G in sf holds
Intersect sf c= G