let I, G, H be set ; :: thesis: for sf being Subset-Family of I st G in sf & G misses H holds
Intersect sf misses H
let sf be Subset-Family of I; :: thesis: ( G in sf & G misses H implies Intersect sf misses H )
assume A1: ( G in sf & G misses H ) ; :: thesis: Intersect sf misses H
then Intersect sf = meet sf by SETFAM_1:def 10;
hence Intersect sf misses H by A1, SETFAM_1:9; :: thesis: verum