theorem Th18: :: MORPH_01:18

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