for I, G being set
for sf being Subset-Family of I st sf <> {} & ( for Z1 being set st Z1 in sf holds
G c= Z1 ) holds
G c= Intersect sf