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

let A, B be non empty binary-image of E; :: thesis: A (-) B = { v where v is Element of E : v + ((- 1) * B) c= A }

thus A (-) B c= { v where v is Element of E : v + ((- 1) * B) c= A } :: according to XBOOLE_0:def 10 :: thesis: { v where v is Element of E : v + ((- 1) * B) c= A } c= A (-) B

assume x in { v where v is Element of E : v + ((- 1) * B) c= A } ; :: thesis: x in A (-) B

then consider v being Element of E such that

A4: ( x = v & v + ((- 1) * B) c= A ) ;

for b being Element of E st b in B holds

v - b in A

let A, B be non empty binary-image of E; :: thesis: A (-) B = { v where v is Element of E : v + ((- 1) * B) c= A }

thus A (-) B c= { v where v is Element of E : v + ((- 1) * B) c= A } :: according to XBOOLE_0:def 10 :: thesis: { v where v is Element of E : v + ((- 1) * B) c= A } c= A (-) B

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { v where v is Element of E : v + ((- 1) * B) c= A } or x in A (-) B )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A (-) B or x in { v where v is Element of E : v + ((- 1) * B) c= A } )

assume x in A (-) B ; :: thesis: x in { v where v is Element of E : v + ((- 1) * B) c= A }

then consider z being Element of E such that

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

z - b in A ) ) ;

z + ((- 1) * B) c= A

end;assume x in A (-) B ; :: thesis: x in { v where v is Element of E : v + ((- 1) * B) c= A }

then consider z being Element of E such that

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

z - b in A ) ) ;

z + ((- 1) * B) c= A

proof

hence
x in { v where v is Element of E : v + ((- 1) * B) c= A }
by A1; :: thesis: verum
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in z + ((- 1) * B) or y in A )

assume y in z + ((- 1) * B) ; :: thesis: y in A

then consider nb being Element of E such that

A2: ( y = z + nb & nb in (- 1) * B ) ;

consider b being Element of E such that

A3: ( nb = (- 1) * b & b in B ) by A2;

z - b in A by A3, A1;

hence y in A by A2, A3, RLVECT_1:16; :: thesis: verum

end;assume y in z + ((- 1) * B) ; :: thesis: y in A

then consider nb being Element of E such that

A2: ( y = z + nb & nb in (- 1) * B ) ;

consider b being Element of E such that

A3: ( nb = (- 1) * b & b in B ) by A2;

z - b in A by A3, A1;

hence y in A by A2, A3, RLVECT_1:16; :: thesis: verum

assume x in { v where v is Element of E : v + ((- 1) * B) c= A } ; :: thesis: x in A (-) B

then consider v being Element of E such that

A4: ( x = v & v + ((- 1) * B) c= A ) ;

for b being Element of E st b in B holds

v - b in A

proof

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

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

then (- 1) * b in (- 1) * B ;

then v + ((- 1) * b) in v + ((- 1) * B) ;

then v - b in v + ((- 1) * B) by RLVECT_1:16;

hence v - b in A by A4; :: thesis: verum

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

then (- 1) * b in (- 1) * B ;

then v + ((- 1) * b) in v + ((- 1) * B) ;

then v - b in v + ((- 1) * B) by RLVECT_1:16;

hence v - b in A by A4; :: thesis: verum