union (rng X) c= A

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in union (rng X) or x in A )
assume x in union (rng X) ; :: thesis: x in A
then consider Y being set such that
A1: ( x in Y & Y in rng X ) by TARSKI:def 4;
thus x in A by A1; :: thesis: verum

end;

hence Union X is Subset of A ; :: thesis: verum