let E be RealLinearSpace; :: thesis: for F being binary-image-family of E

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

let F be binary-image-family of E; :: thesis: for B being non empty binary-image of E holds (erosion B) . (meet F) = meet { ((erosion B) . X) where X is binary-image of E : X in F }

let B be non empty binary-image of E; :: thesis: (erosion B) . (meet F) = meet { ((erosion B) . X) where X is binary-image of E : X in F }

A1: for x being object holds

( x in { (X (-) B) where X is binary-image of E : X in F } iff x in { ((erosion B) . X) where X is binary-image of E : X in F } )

.= meet { (X (-) B) where X is binary-image of E : X in F } by Th18

.= meet { ((erosion B) . X) where X is binary-image of E : X in F } by A1, TARSKI:2 ; :: thesis: verum

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

let F be binary-image-family of E; :: thesis: for B being non empty binary-image of E holds (erosion B) . (meet F) = meet { ((erosion B) . X) where X is binary-image of E : X in F }

let B be non empty binary-image of E; :: thesis: (erosion B) . (meet F) = meet { ((erosion B) . X) where X is binary-image of E : X in F }

A1: for x being object holds

( x in { (X (-) B) where X is binary-image of E : X in F } iff x in { ((erosion B) . X) where X is binary-image of E : X in F } )

proof

thus (erosion B) . (meet F) =
(meet F) (-) B
by Def3
let x be object ; :: thesis: ( x in { (X (-) B) where X is binary-image of E : X in F } iff x in { ((erosion B) . X) where X is binary-image of E : X in F } )

then consider X being binary-image of E such that

A3: ( x = (erosion B) . X & X in F ) ;

( x = X (-) B & X in F ) by A3, Def3;

hence x in { (W (-) B) where W is binary-image of E : W in F } ; :: thesis: verum

end;hereby :: thesis: ( x in { ((erosion B) . X) where X is binary-image of E : X in F } implies x in { (X (-) B) where X is binary-image of E : X in F } )

assume
x in { ((erosion B) . X) where X is binary-image of E : X in F }
; :: thesis: x in { (X (-) B) where X is binary-image of E : X in F } assume
x in { (X (-) B) where X is binary-image of E : X in F }
; :: thesis: x in { ((erosion B) . W) where W is binary-image of E : W in F }

then consider X being binary-image of E such that

A2: ( x = X (-) B & X in F ) ;

( x = (erosion B) . X & X in F ) by A2, Def3;

hence x in { ((erosion B) . W) where W is binary-image of E : W in F } ; :: thesis: verum

end;then consider X being binary-image of E such that

A2: ( x = X (-) B & X in F ) ;

( x = (erosion B) . X & X in F ) by A2, Def3;

hence x in { ((erosion B) . W) where W is binary-image of E : W in F } ; :: thesis: verum

then consider X being binary-image of E such that

A3: ( x = (erosion B) . X & X in F ) ;

( x = X (-) B & X in F ) by A3, Def3;

hence x in { (W (-) B) where W is binary-image of E : W in F } ; :: thesis: verum

.= meet { (X (-) B) where X is binary-image of E : X in F } by Th18

.= meet { ((erosion B) . X) where X is binary-image of E : X in F } by A1, TARSKI:2 ; :: thesis: verum