let E be RealLinearSpace; :: thesis: for F being binary-image-family of E
for B being non empty binary-image of E holds (meet F) (+) B c= meet { (X (+) B) 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 (meet F) (+) B c= meet { (X (+) B) where X is binary-image of E : X in F }
let B be non empty binary-image of E; :: thesis: (meet F) (+) B c= meet { (X (+) B) where X is binary-image of E : X in F }

per cases ( F = {} or F <> {} ) ;

suppose G1: F = {} ; :: thesis: (meet F) (+) B c= meet { (X (+) B) where X is binary-image of E : X in F }

reconsider Z = meet F as Subset of E ;
meet F = {} by G1, SETFAM_1:def 1;
then Z (+) B = {} by LM0010;
hence (meet F) (+) B c= meet { (X (+) B) where X is binary-image of E : X in F } by XBOOLE_1:2; :: thesis: verum

end;

suppose F <> {} ; :: thesis: (meet F) (+) B c= meet { (X (+) B) where X is binary-image of E : X in F }

then consider W0 being set such that
P0: W0 in F by XBOOLE_0:def 1;
reconsider W0 = W0 as binary-image of E by P0;
P2: W0 (+) B in { (W (+) B) where W is binary-image of E : W in F } by P0;

now :: thesis: for x being set st x in (meet F) (+) B holds
x in meet { (W (+) B) where W is binary-image of E : W in F }

let x be set ; :: thesis: ( x in (meet F) (+) B implies x in meet { (W (+) B) where W is binary-image of E : W in F } )
assume x in (meet F) (+) B ; :: thesis: x in meet { (W (+) B) where W is binary-image of E : W in F }
then consider f, b being Element of E such that
P1: ( x = f + b & f in meet F & b in B ) ;

now :: thesis: for Y being set st Y in { (X (+) B) where X is binary-image of E : X in F } holds
x in Y

let Y be set ; :: thesis: ( Y in { (X (+) B) where X is binary-image of E : X in F } implies x in Y )
assume Y in { (X (+) B) where X is binary-image of E : X in F } ; :: thesis: x in Y
then consider X being binary-image of E such that
P3: ( Y = X (+) B & X in F ) ;
meet F c= X by P3, SETFAM_1:3;
hence x in Y by P1, P3; :: thesis: verum

end;

hence x in meet { (W (+) B) where W is binary-image of E : W in F } by P2, SETFAM_1:def 1; :: thesis: verum

end;

hence (meet F) (+) B c= meet { (X (+) B) where X is binary-image of E : X in F } by TARSKI:def 3; :: thesis: verum

end;

end;