:: deftheorem defines sequence_univers CLASSES4:def 11 :
sequence_univers = sequence_univers {};