theorem :: MORPH_01:19

for E being RealLinearSpace
for F being binary-image-family of E
for B being non empty binary-image of E holds meet { (B (-) X) where X is binary-image of E : X in F } c= B (-) (meet F)