:: deftheorem defines super_univers CLASSES4:def 12 :
super_univers = GrothendieckUniverse sequence_univers;