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;
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 }
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
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
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;
hence x in meet { (b + A) where b is Element of E : b in B } by ; :: thesis: verum
end;
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 (-) B
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
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 ;
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
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 ;
then consider a being Element of E such that
A9: ( x0 = b + a & a in A ) ;
thus x0 - b in A by ; :: 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 ; :: thesis: verum