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 set such that
P01: g in B by XBOOLE_0:def 1;
reconsider g = g as Element of E by P01;
P02: g + A in { (b + A) where b is Element of E : b in B } by P01;

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

let x be set ; :: 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
P1: ( 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

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
A2: ( Y = b + A & b in B ) ;
A3: z - b in A by P1, A2;
z = b + (z - b) by RLVECT_4:1;
hence z in Y by A3, A2; :: thesis: verum

end;

hence x in meet { (b + A) where b is Element of E : b in B } by P1, P02, SETFAM_1:def 1; :: thesis: verum

end;

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

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

let x be set ; :: thesis: ( x in meet { (b + A) where b is Element of E : b in B } implies x in A (-) B )
assume P0: 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
P11: S in { (b + A) where b is Element of E : b in B } by P02;
consider d being Element of E such that
P12: ( S = d + A & d in B ) by P11;
x in S by P0, P11, SETFAM_1:def 1;
then reconsider x0 = x as Element of E by P12;
for b being Element of E st b in B holds
x0 - b in A

proof

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 P0, SETFAM_1:def 1;
then consider a being Element of E such that
X1: ( x0 = b + a & a in A ) ;
thus x0 - b in A by X1, RLVECT_4:1; :: thesis: verum

end;

hence x in A (-) B ; :: thesis: verum

end;

hence meet { (b + A) where b is Element of E : b in B } c= A (-) B by TARSKI:def 3; :: thesis: verum