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