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 non-empty
thus G is non-empty by A1; :: thesis: verum