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