let UN be Universe; :: thesis: UN is Grothendieck of {}
{} in UN by Th13;
hence UN is Grothendieck of {} by CLASSES3:def 4; :: thesis: verum