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
proof
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
proof
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;
hence x in { v where v is Element of E : v + ((- 1) * B) c= A } by A1; :: thesis: verum
end;
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 )
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
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;
hence x in A (-) B by A4; :: thesis: verum