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

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

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

A6: for W being binary-image of E st W in F holds

x in B (-) W

then reconsider z = x as Element of E ;

for f being Element of E st f in union F holds

z - f in B

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

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

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

hence
x in meet { (B (-) W) where W is binary-image of E : W in F }
by A2, SETFAM_1:def 1; :: thesis: verumx 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 ) ;

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

hence
x in Y
by A3, A4; :: thesis: verumz - 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;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

A6: for W being binary-image of E st W in F holds

x in B (-) W

proof

x in B (-) W0
by A1, A6;
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;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

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

hence
x in B (-) (union F)
; :: thesis: verum
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;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