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 AS: A c= B ; :: thesis: (erosion C) . A c= (erosion C) . B
P1: (erosion C) . A = A (-) C by def030;
(erosion C) . B = B (-) C by def030;
hence (erosion C) . A c= (erosion C) . B by P1, AS, Th118; :: thesis: verum