set G = UN;
( UN is axiom_GU4 & Union x = union (rng x) ) ;
hence Union x is Element of UN ; :: thesis: verum