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