let E be RealLinearSpace; :: thesis: for F being binary-image-family of E

for B being non empty binary-image of E holds meet { (B (-) X) where X is binary-image of E : X in F } c= B (-) (meet F)

let F be binary-image-family of E; :: thesis: for B being non empty binary-image of E holds meet { (B (-) X) where X is binary-image of E : X in F } c= B (-) (meet F)

let B be non empty binary-image of E; :: thesis: meet { (B (-) X) where X is binary-image of E : X in F } c= B (-) (meet F)

for B being non empty binary-image of E holds meet { (B (-) X) where X is binary-image of E : X in F } c= B (-) (meet F)

let F be binary-image-family of E; :: thesis: for B being non empty binary-image of E holds meet { (B (-) X) where X is binary-image of E : X in F } c= B (-) (meet F)

let B be non empty binary-image of E; :: thesis: meet { (B (-) X) where X is binary-image of E : X in F } c= B (-) (meet F)

per cases
( F = {} or F <> {} )
;

end;

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

reconsider Z = meet F as Subset of E ;

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

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

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

proof

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

then consider x being object such that

A2: x in { (B (-) X) where X is binary-image of E : X in F } by XBOOLE_0:def 1;

ex X being binary-image of E st

( x = B (-) X & X in F ) by A2;

hence contradiction by A1; :: thesis: verum

end;then consider x being object such that

A2: x in { (B (-) X) where X is binary-image of E : X in F } by XBOOLE_0:def 1;

ex X being binary-image of E st

( x = B (-) X & X in F ) by A2;

hence contradiction by A1; :: thesis: verum

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

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

then consider W0 being object such that

A3: W0 in F by XBOOLE_0:def 1;

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

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in meet { (B (-) X) where X is binary-image of E : X in F } or x in B (-) (meet F) )

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

A5: 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 meet F holds

z - f in B

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

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

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in meet { (B (-) X) where X is binary-image of E : X in F } or x in B (-) (meet F) )

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

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

x in B (-) W

proof

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

then reconsider z = x as Element of E ;

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

z - f in B

proof

hence
x in B (-) (meet F)
; :: thesis: verum
let f be Element of E; :: thesis: ( f in meet F implies z - f in B )

assume A7: f in meet F ; :: thesis: z - f in B

A8: meet F c= W0 by A3, SETFAM_1:3;

consider zz being Element of E such that

A9: ( z = zz & ( for w being Element of E st w in W0 holds

zz - w in B ) ) by A6;

thus z - f in B by A9, A7, A8; :: thesis: verum

end;assume A7: f in meet F ; :: thesis: z - f in B

A8: meet F c= W0 by A3, SETFAM_1:3;

consider zz being Element of E such that

A9: ( z = zz & ( for w being Element of E st w in W0 holds

zz - w in B ) ) by A6;

thus z - f in B by A9, A7, A8; :: thesis: verum