let E be RealLinearSpace; :: thesis: for F being binary-image-family of E
for B being non empty binary-image of E st F <> {} holds
B (-) (union F) = meet { (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 st F <> {} holds
B (-) (union F) = meet { (B (-) X) where X is binary-image of E : X in F }
let B be non empty binary-image of E; :: thesis: ( F <> {} implies B (-) (union F) = meet { (B (-) X) where X is binary-image of E : X in F } )
assume F <> {} ; :: thesis: B (-) (union F) = meet { (B (-) X) 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: B (-) W0 in { (B (-) X) where X is binary-image of E : X in F } by P0;
for x being set holds
( x in B (-) (union F) iff x in meet { (B (-) X) where X is binary-image of E : X in F } )

proof

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

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

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

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

let Y be set ; :: thesis: ( Y in { (B (-) X) where X is binary-image of E : X in F } implies x in Y )
assume Y in { (B (-) X) where X is binary-image of E : X in F } ; :: thesis: x in Y
then consider X being binary-image of E such that
Q2: ( Y = B (-) X & X in F ) ;

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

let f be Element of E; :: thesis: ( f in X implies z - f in B )
assume f in X ; :: thesis: z - f in B
then f in union F by Q2, TARSKI:def 4;
hence z - f in B by Q1; :: thesis: verum

end;

hence x in Y by Q1, Q2; :: thesis: verum

end;

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

end;

assume X1: x in meet { (B (-) W) where W is binary-image of E : W in F } ; :: thesis: x in B (-) (union F)
Q1: 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 X1, SETFAM_1:def 1; :: thesis: verum

end;

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

proof

let f be Element of E; :: thesis: ( f in union F implies z - f in B )
assume f in union F ; :: thesis: z - f in B
then consider W being set such that
Q4: ( f in W & W in F ) by TARSKI:def 4;
reconsider W = W as binary-image of E by Q4;
z in B (-) W by Q1, Q4;
then consider w being Element of E such that
Q7: ( z = w & ( for f being Element of E st f in W holds
w - f in B ) ) ;
thus z - f in B by Q4, Q7; :: thesis: verum

end;

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

end;

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