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