set G = the GeneratorSet of T;
take X = Union the GeneratorSet of T; :: thesis: ex G being GeneratorSet of T st X = Union G
take the GeneratorSet of T ; :: thesis: X = Union the GeneratorSet of T
thus X = Union the GeneratorSet of T ; :: thesis: verum