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 }

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

end;

suppose A1:
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 ;

A2: meet F = {} by A1, SETFAM_1:def 1;

{ (X (-) B) where X is binary-image of E : X in F } = {}

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

end;A2: meet F = {} by A1, SETFAM_1:def 1;

{ (X (-) B) where X is binary-image of E : X in F } = {}

proof

then
{} = meet { (X (-) B) where X is binary-image of E : X in F }
by SETFAM_1:def 1;
assume
{ (X (-) B) where X is binary-image of E : X in F } <> {}
; :: thesis: contradiction

then consider x being object such that

A3: 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 A3;

hence contradiction by A1; :: thesis: verum

end;then consider x being object such that

A3: 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 A3;

hence contradiction by A1; :: thesis: verum

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

suppose A4:
F <> {}
; :: thesis: (meet F) (-) B = meet { (X (-) B) where X is binary-image of E : X in F }

then consider W0 being object such that

A5: W0 in F by XBOOLE_0:def 1;

reconsider W0 = W0 as binary-image of E by A5;

A6: W0 (-) B in { (W (-) B) where W is binary-image of E : W in F } by A5;

for x being object holds

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

end;A5: W0 in F by XBOOLE_0:def 1;

reconsider W0 = W0 as binary-image of E by A5;

A6: W0 (-) B in { (W (-) B) where W is binary-image of E : W in F } by A5;

for x being object holds

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

proof

hence
(meet F) (-) B = meet { (X (-) B) where X is binary-image of E : X in F }
by TARSKI:2; :: thesis: verum
let x be object ; :: thesis: ( x in (meet F) (-) B iff x in meet { (W (-) B) where W is binary-image of E : W in F } )

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

x in W (-) B

then reconsider z = x as Element of E ;

for b being Element of E st b in B holds

z - b in meet F

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

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

A7: ( x = z & ( for b being Element of E st b in B holds

z - b in meet F ) ) ;

end;then consider z being Element of E such that

A7: ( 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

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

A8: ( Y = X (-) B & X in F ) ;

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

A8: ( Y = X (-) B & X in F ) ;

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

z - b in X

hence
x in Y
by A8, A7; :: thesis: verumz - 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 A9: z - b in meet F by A7;

meet F c= X by A8, SETFAM_1:3;

hence z - b in X by A9; :: thesis: verum

end;assume b in B ; :: thesis: z - b in X

then A9: z - b in meet F by A7;

meet F c= X by A8, SETFAM_1:3;

hence z - b in X by A9; :: thesis: verum

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

x in W (-) B

proof

x in W0 (-) B
by A5, A11;
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 A10, SETFAM_1:def 1; :: thesis: verum

end;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 A10, SETFAM_1:def 1; :: thesis: verum

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

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

A12: ( b in B & not z - b in meet F ) ;

consider X being set such that

A13: ( X in F & not z - b in X ) by A4, A12, SETFAM_1:def 1;

reconsider X = X as binary-image of E by A13;

z in X (-) B by A13, A11;

then consider zz being Element of E such that

A14: ( z = zz & ( for b being Element of E st b in B holds

zz - b in X ) ) ;

thus contradiction by A14, A12, A13; :: thesis: verum

end;( b in B & not z - b in meet F ) ; :: thesis: contradiction

then consider b being Element of E such that

A12: ( b in B & not z - b in meet F ) ;

consider X being set such that

A13: ( X in F & not z - b in X ) by A4, A12, SETFAM_1:def 1;

reconsider X = X as binary-image of E by A13;

z in X (-) B by A13, A11;

then consider zz being Element of E such that

A14: ( z = zz & ( for b being Element of E st b in B holds

zz - b in X ) ) ;

thus contradiction by A14, A12, A13; :: thesis: verum