let E be RealLinearSpace; :: thesis: for F being binary-image-family of E
for B being non empty binary-image of E holds union { (X (-) B) where X is binary-image of E : X in F } c= (union F) (-) B
let F be binary-image-family of E; :: thesis: for B being non empty binary-image of E holds union { (X (-) B) where X is binary-image of E : X in F } c= (union F) (-) B
let B be non empty binary-image of E; :: thesis: union { (X (-) B) where X is binary-image of E : X in F } c= (union F) (-) B
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union { (X (-) B) where X is binary-image of E : X in F } or x in (union F) (-) B )
assume x in union { (X (-) B) where X is binary-image of E : X in F } ; :: thesis: x in (union F) (-) B
then consider Y being set such that
A1: ( x in Y & Y in { (X (-) B) where X is binary-image of E : X in F } ) by TARSKI:def 4;
consider W being binary-image of E such that
A2: ( Y = W (-) B & W in F ) by A1;
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 W ) ) by A1, A2;
now :: thesis: for b being Element of E st b in B holds
z - b in union F
let b be Element of E; :: thesis: ( b in B implies z - b in union F )
assume b in B ; :: thesis: z - b in union F
then A4: z - b in W by A3;
W c= union F by A2, ZFMISC_1:74;
hence z - b in union F by A4; :: thesis: verum
end;
hence x in (union F) (-) B by A3; :: thesis: verum