set SU = GrothendieckUniverse sequence_univers;
( NAT in SETS & SETS in GrothendieckUniverse sequence_univers & GrothendieckUniverse sequence_univers is axiom_GU1 ) by Th103, Th72;
hence GrothendieckUniverse sequence_univers is non trivial Universe by Def6; :: thesis: verum