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

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in (union FR) .: X or a in union { (R .: X) where R is Subset of [:A,B:] : R in FR } )
assume a in (union FR) .: X ; :: thesis: a in union { (R .: X) where R is Subset of [:A,B:] : R in FR }
then consider x being object such that
A1: [x,a] in union FR and
A2: x in X by RELAT_1:def 13;
consider S being set such that
A3: [x,a] in S and
A4: S in FR by A1, TARSKI:def 4;
reconsider S = S as Subset of [:A,B:] by A4;
ex P being set st
( a in P & P in { (T .: X) where T is Subset of [:A,B:] : T in FR } )

proof

set P = S .: X;
A5: a in S .: X by A2, A3, RELAT_1:def 13;
S .: X in { (T .: X) where T is Subset of [:A,B:] : T in FR } by A4;
hence ex P being set st
( a in P & P in { (T .: X) where T is Subset of [:A,B:] : T in FR } ) by A5; :: thesis: verum

end;

hence a in union { (R .: X) where R is Subset of [:A,B:] : R in FR } by TARSKI:def 4; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in union { (R .: X) where R is Subset of [:A,B:] : R in FR } or a in (union FR) .: X )
assume a in union { (R .: X) where R is Subset of [:A,B:] : R in FR } ; :: thesis: a in (union FR) .: X
then consider P being set such that
A6: a in P and
A7: P in { (R .: X) where R is Subset of [:A,B:] : R in FR } by TARSKI:def 4;
consider R being Subset of [:A,B:] such that
A8: P = R .: X and
A9: R in FR by A7;
consider x being object such that
A10: [x,a] in R and
A11: x in X by A6, A8, RELAT_1:def 13;
ex x being set st
( x in X & [x,a] in union FR )

proof

take x ; :: thesis: ( x is set & x in X & [x,a] in union FR )
thus ( x is set & x in X & [x,a] in union FR ) by A9, A10, A11, TARSKI:def 4; :: thesis: verum

end;

hence a in (union FR) .: X by RELAT_1:def 13; :: thesis: verum