for U being Universe holds Tarski-Class U is Universe by Th47;