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