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 }

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 <> {} )
;

end;

suppose A1:
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 A1, SETFAM_1:def 1;

then Z (+) B = {} by Th1;

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

end;meet F = {} by A1, SETFAM_1:def 1;

then Z (+) B = {} by Th1;

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

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

then consider W0 being object such that

A2: W0 in F by XBOOLE_0:def 1;

reconsider W0 = W0 as binary-image of E by A2;

A3: W0 (+) B in { (W (+) B) where W is binary-image of E : W in F } by A2;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (meet F) (+) B or x in meet { (X (+) B) where X is binary-image of E : X in F } )

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

then consider f, b being Element of E such that

A4: ( x = f + b & f in meet F & b in B ) ;

end;A2: W0 in F by XBOOLE_0:def 1;

reconsider W0 = W0 as binary-image of E by A2;

A3: W0 (+) B in { (W (+) B) where W is binary-image of E : W in F } by A2;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (meet F) (+) B or x in meet { (X (+) B) where X is binary-image of E : X in F } )

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

then consider f, b being Element of E such that

A4: ( 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

hence
x in meet { (W (+) B) where W is binary-image of E : W in F }
by A3, SETFAM_1:def 1; :: thesis: verumx 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

A5: ( Y = X (+) B & X in F ) ;

meet F c= X by A5, SETFAM_1:3;

hence x in Y by A4, A5; :: thesis: verum

end;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

A5: ( Y = X (+) B & X in F ) ;

meet F c= X by A5, SETFAM_1:3;

hence x in Y by A4, A5; :: thesis: verum