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 set ; :: 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 set such that
A1: ( [x,a] in union FR & x in X ) by RELAT_1:def 13;
consider S being set such that
A2: ( [x,a] in S & S in FR ) by A1, TARSKI:def 4;
reconsider S = S as Subset of [:A,B:] by A2;
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;
A3: a in S .: X by A1, A2, RELAT_1:def 13;
S .: X in { (T .: X) where T is Subset of [:A,B:] : T in FR } by A2;
hence ex P being set st
( a in P & P in { (T .: X) where T is Subset of [:A,B:] : T in FR } ) by A3; :: 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 set ; :: 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
A4: ( a in P & 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
A5: ( P = R .: X & R in FR ) by A4;
consider x being set such that
A6: ( [x,a] in R & x in X ) by A4, A5, RELAT_1:def 13;
ex x being set st
( x in X & [x,a] in union FR )

proof

take x ; :: thesis: ( x in X & [x,a] in union FR )
thus ( x in X & [x,a] in union FR ) by A5, A6, TARSKI:def 4; :: thesis: verum

end;

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