let A be set ; :: thesis: for F being Subset-Family of A
for R being Relation holds R .: (union F) = union { (R .: X) where X is Subset of A : X in F }
let F be Subset-Family of A; :: thesis: for R being Relation holds R .: (union F) = union { (R .: X) where X is Subset of A : X in F }
let R be Relation; :: thesis: R .: (union F) = union { (R .: X) where X is Subset of A : X in F }
thus R .: (union F) c= union { (R .: f) where f is Subset of A : f in F } :: according to XBOOLE_0:def 10 :: thesis: union { (R .: X) where X is Subset of A : X in F } c= R .: (union F)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in R .: (union F) or y in union { (R .: f) where f is Subset of A : f in F } )
assume y in R .: (union F) ; :: thesis: y in union { (R .: f) where f is Subset of A : f in F }
then consider x being object such that
A1: [x,y] in R and
A2: x in union F by RELAT_1:def 13;
consider Y being set such that
A3: x in Y and
A4: Y in F by A2, TARSKI:def 4;
set Z = R .: Y;
A5: y in R .: Y by A1, A3, RELAT_1:def 13;
R .: Y in { (R .: f) where f is Subset of A : f in F } by A4;
hence y in union { (R .: f) where f is Subset of A : f in F } by A5, TARSKI:def 4; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in union { (R .: X) where X is Subset of A : X in F } or y in R .: (union F) )
assume y in union { (R .: f) where f is Subset of A : f in F } ; :: thesis: y in R .: (union F)
then consider Y being set such that
A6: y in Y and
A7: Y in { (R .: f) where f is Subset of A : f in F } by TARSKI:def 4;
consider f being Subset of A such that
A8: Y = R .: f and
A9: f in F by A7;
consider x being object such that
A10: [x,y] in R and
A11: x in f by A6, A8, RELAT_1:def 13;
x in union F by A9, A11, TARSKI:def 4;
hence y in R .: (union F) by A10, RELAT_1:def 13; :: thesis: verum