let E be RealLinearSpace; :: thesis: for A, B being non empty binary-image of E holds A (-) B = meet { (b + A) where b is Element of E : b in B }

let A, B be non empty binary-image of E; :: thesis: A (-) B = meet { (b + A) where b is Element of E : b in B }

consider g being object such that

A1: g in B by XBOOLE_0:def 1;

reconsider g = g as Element of E by A1;

A2: g + A in { (b + A) where b is Element of E : b in B } by A1;

let A, B be non empty binary-image of E; :: thesis: A (-) B = meet { (b + A) where b is Element of E : b in B }

consider g being object such that

A1: g in B by XBOOLE_0:def 1;

reconsider g = g as Element of E by A1;

A2: g + A in { (b + A) where b is Element of E : b in B } by A1;

now :: thesis: for x being object st x in A (-) B holds

x in meet { (b + A) where b is Element of E : b in B }

hence
A (-) B c= meet { (b + A) where b is Element of E : b in B }
; :: according to XBOOLE_0:def 10 :: thesis: meet { (b + A) where b is Element of E : b in B } c= A (-) Bx in meet { (b + A) where b is Element of E : b in B }

let x be object ; :: thesis: ( x in A (-) B implies x in meet { (b + A) where b is Element of E : b in B } )

assume x in A (-) B ; :: thesis: x in meet { (b + A) where b is Element of E : b in B }

then consider z being Element of E such that

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

z - b in A ) ) ;

for Y being set st Y in { (b + A) where b is Element of E : b in B } holds

z in Y

end;assume x in A (-) B ; :: thesis: x in meet { (b + A) where b is Element of E : b in B }

then consider z being Element of E such that

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

z - b in A ) ) ;

for Y being set st Y in { (b + A) where b is Element of E : b in B } holds

z in Y

proof

hence
x in meet { (b + A) where b is Element of E : b in B }
by A3, A2, SETFAM_1:def 1; :: thesis: verum
let Y be set ; :: thesis: ( Y in { (b + A) where b is Element of E : b in B } implies z in Y )

assume Y in { (b + A) where b is Element of E : b in B } ; :: thesis: z in Y

then consider b being Element of E such that

A4: ( Y = b + A & b in B ) ;

A5: z - b in A by A3, A4;

z = b + (z - b) by RLVECT_4:1;

hence z in Y by A5, A4; :: thesis: verum

end;assume Y in { (b + A) where b is Element of E : b in B } ; :: thesis: z in Y

then consider b being Element of E such that

A4: ( Y = b + A & b in B ) ;

A5: z - b in A by A3, A4;

z = b + (z - b) by RLVECT_4:1;

hence z in Y by A5, A4; :: thesis: verum

now :: thesis: for x being object st x in meet { (b + A) where b is Element of E : b in B } holds

x in A (-) B

hence
meet { (b + A) where b is Element of E : b in B } c= A (-) B
; :: thesis: verumx in A (-) B

let x be object ; :: thesis: ( x in meet { (b + A) where b is Element of E : b in B } implies x in A (-) B )

assume A6: x in meet { (b + A) where b is Element of E : b in B } ; :: thesis: x in A (-) B

consider S being set such that

A7: S in { (b + A) where b is Element of E : b in B } by A2;

consider d being Element of E such that

A8: ( S = d + A & d in B ) by A7;

x in S by A6, A7, SETFAM_1:def 1;

then reconsider x0 = x as Element of E by A8;

for b being Element of E st b in B holds

x0 - b in A

end;assume A6: x in meet { (b + A) where b is Element of E : b in B } ; :: thesis: x in A (-) B

consider S being set such that

A7: S in { (b + A) where b is Element of E : b in B } by A2;

consider d being Element of E such that

A8: ( S = d + A & d in B ) by A7;

x in S by A6, A7, SETFAM_1:def 1;

then reconsider x0 = x as Element of E by A8;

for b being Element of E st b in B holds

x0 - b in A

proof

hence
x in A (-) B
; :: thesis: verum
let b be Element of E; :: thesis: ( b in B implies x0 - b in A )

assume b in B ; :: thesis: x0 - b in A

then b + A in { (f + A) where f is Element of E : f in B } ;

then x in b + A by A6, SETFAM_1:def 1;

then consider a being Element of E such that

A9: ( x0 = b + a & a in A ) ;

thus x0 - b in A by A9, RLVECT_4:1; :: thesis: verum

end;assume b in B ; :: thesis: x0 - b in A

then b + A in { (f + A) where f is Element of E : f in B } ;

then x in b + A by A6, SETFAM_1:def 1;

then consider a being Element of E such that

A9: ( x0 = b + a & a in A ) ;

thus x0 - b in A by A9, RLVECT_4:1; :: thesis: verum