theorem :: MORPH_01:15

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