:: deftheorem Def3 defines erosion MORPH_01:def 3 :
for E being RealLinearSpace
for B being binary-image of E
for b₃ being Function of (bool the carrier of E),(bool the carrier of E) holds
( b₃ = erosion B iff for A being binary-image of E holds b₃ . A = A (-) B );