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 (-) () = 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 (-) () = 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 (-) () = meet { (B (-) X) where X is binary-image of E : X in F } )
assume F <> {} ; :: thesis: B (-) () = 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 (-) () 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 (-) () 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 (-) () )
assume x in B (-) () ; :: 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 ;
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 ; :: thesis: verum
end;
assume A5: x in meet { (B (-) W) where W is binary-image of E : W in F } ; :: thesis: x in B (-) ()
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 ; :: 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 (-) () ; :: thesis: verum
end;
hence B (-) () = meet { (B (-) X) where X is binary-image of E : X in F } by TARSKI:2; :: thesis: verum