let I, G be set ; :: thesis: 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
let sf be Subset-Family of I; :: thesis: ( sf <> {} & ( for Z1 being set st Z1 in sf holds
G c= Z1 ) implies G c= Intersect sf )
assume that
A1: sf <> {} and
A2: for Z1 being set st Z1 in sf holds
G c= Z1 ; :: thesis: G c= Intersect sf
Intersect sf = meet sf by A1, SETFAM_1:def 9;
hence G c= Intersect sf by A1, A2, SETFAM_1:5; :: thesis: verum