let E be RealLinearSpace; :: thesis: for A, B, C being non empty binary-image of E st A c= B holds
(erosion C) . A c= (erosion C) . B
let A, B, C be non empty binary-image of E; :: thesis: ( A c= B implies (erosion C) . A c= (erosion C) . B )
assume A1: A c= B ; :: thesis: (erosion C) . A c= (erosion C) . B
A2: (erosion C) . A = A (-) C by Def3;
(erosion C) . B = B (-) C by Def3;
hence (erosion C) . A c= (erosion C) . B by A2, A1, Th22; :: thesis: verum