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 = 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 = 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 = 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 = meet { (X (-) B) where X is binary-image of E : X in F }

reconsider Z = meet F as Subset of E ;
G2: meet F = {} by G1, SETFAM_1:def 1;
{ (X (-) B) where X is binary-image of E : X in F } = {}

proof

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

end;

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

end;

suppose G2: F <> {} ; :: thesis: (meet F) (-) B = 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;
for x being set holds
( x in (meet F) (-) B iff x in meet { (W (-) B) where W is binary-image of E : W in F } )

proof

let x be set ; :: thesis: ( x in (meet F) (-) B iff x in meet { (W (-) B) where W is binary-image of E : W in F } )

hereby :: thesis: ( x in meet { (W (-) B) where W is binary-image of E : W in F } implies x in (meet F) (-) B )

assume x in (meet F) (-) B ; :: thesis: x in meet { (W (-) B) where W is binary-image of E : W in F }
then consider z being Element of E such that
Q1: ( x = z & ( for b being Element of E st b in B holds
z - b in meet F ) ) ;

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

now :: thesis: for b being Element of E st b in B holds
z - b in X

let b be Element of E; :: thesis: ( b in B implies z - b in X )
assume b in B ; :: thesis: z - b in X
then X1: z - b in meet F by Q1;
meet F c= X by P3, SETFAM_1:3;
hence z - b in X by X1; :: thesis: verum

end;

hence x in Y by P3, Q1; :: 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;

assume X1: x in meet { (W (-) B) where W is binary-image of E : W in F } ; :: thesis: x in (meet F) (-) B
Q1: for W being binary-image of E st W in F holds
x in W (-) B

proof

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

end;

x in W0 (-) B by P0, Q1;
then reconsider z = x as Element of E ;
for b being Element of E st b in B holds
z - b in meet F

proof

assume ex b being Element of E st
( b in B & not z - b in meet F ) ; :: thesis: contradiction
then consider b being Element of E such that
D2: ( b in B & not z - b in meet F ) ;
consider X being set such that
Q5: ( X in F & not z - b in X ) by G2, D2, SETFAM_1:def 1;
reconsider X = X as binary-image of E by Q5;
z in X (-) B by Q5, Q1;
then consider zz being Element of E such that
Q70: ( z = zz & ( for b being Element of E st b in B holds
zz - b in X ) ) ;
thus contradiction by Q70, D2, Q5; :: thesis: verum

end;

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

end;

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

end;

end;