let I be set ; :: thesis: for sf being Subset-Family of I st sf <> {} holds
Intersect sf c= union sf
let sf be Subset-Family of I; :: thesis: ( sf <> {} implies Intersect sf c= union sf )
assume sf <> {} ; :: thesis: Intersect sf c= union sf
then Intersect sf = meet sf by SETFAM_1:def 9;
hence Intersect sf c= union sf by SETFAM_1:2; :: thesis: verum