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 object such that
A1: W0 in F by XBOOLE_0:def 1;
reconsider W0 = W0 as binary-image of E by A1;
A2: B (-) W0 in { (B (-) X) where X is binary-image of E : X in F } by A1;
for x being object 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 object ; :: 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
A3: ( 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
A4: ( 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 A4, TARSKI:def 4;
hence z - f in B by A3; :: thesis: verum

end;

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

end;

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

end;

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

end;

x in B (-) W0 by A1, A6;
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
A7: ( f in W & W in F ) by TARSKI:def 4;
reconsider W = W as binary-image of E by A7;
z in B (-) W by A6, A7;
then consider w being Element of E such that
A8: ( z = w & ( for f being Element of E st f in W holds
w - f in B ) ) ;
thus z - f in B by A7, A8; :: 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:2; :: thesis: verum