Union F1 = union (rng F1) by CARD_3:def 4;
hence Union F1 is Subset of X ; :: thesis: verum