the Sorts of U1 is GeneratorSet of U1 by MSAFREE2:6;
then consider G being GeneratorSet of U1 such that
A1: G = the Sorts of U1 ;
take G ; :: thesis: G is V2()
thus G is V2() by A1; :: thesis: verum