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

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

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

reconsider Z = meet F as Subset of E ;
{ (B (-) X) where X is binary-image of E : X in F } = {}

proof

assume { (B (-) X) where X is binary-image of E : X in F } <> {} ; :: thesis: contradiction
then consider x being object such that
A2: x in { (B (-) X) where X is binary-image of E : X in F } by XBOOLE_0:def 1;
ex X being binary-image of E st
( x = B (-) X & X in F ) by A2;
hence contradiction by A1; :: thesis: verum

end;

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

end;

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

then consider W0 being object such that
A3: W0 in F by XBOOLE_0:def 1;
reconsider W0 = W0 as binary-image of E by A3;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in meet { (B (-) X) where X is binary-image of E : X in F } or x in B (-) (meet F) )
assume A4: x in meet { (B (-) W) where W is binary-image of E : W in F } ; :: thesis: x in B (-) (meet F)
A5: for W being binary-image of E st W in F holds
x in B (-) W

proof

let W be binary-image of E; :: thesis: ( W in F implies x in B (-) W )
assume W in F ; :: thesis: x in B (-) W
then B (-) W in { (B (-) D) where D is binary-image of E : D in F } ;
hence x in B (-) W by A4, SETFAM_1:def 1; :: thesis: verum

end;

A6: x in B (-) W0 by A3, A5;
then reconsider z = x as Element of E ;
for f being Element of E st f in meet F holds
z - f in B

proof

let f be Element of E; :: thesis: ( f in meet F implies z - f in B )
assume A7: f in meet F ; :: thesis: z - f in B
A8: meet F c= W0 by A3, SETFAM_1:3;
consider zz being Element of E such that
A9: ( z = zz & ( for w being Element of E st w in W0 holds
zz - w in B ) ) by A6;
thus z - f in B by A9, A7, A8; :: thesis: verum

end;

hence x in B (-) (meet F) ; :: thesis: verum

end;

end;