union (rng X) c= A

proof

let x be object ; :: 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 ex Y being set st
( x in Y & Y in rng X ) by TARSKI:def 4;
hence x in A ; :: thesis: verum

end;

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