( REAL_Music is satisfying_harmonic_closed & REAL_Music is satisfying_Nat & REAL_Music is satisfying_commutativity & REAL_Music is satisfying_tonic & REAL_Music is satisfying_interval & REAL_Music is satisfying_equiv & REAL_Music is satisfying_Real ) by Th9, Th4, Th12, Th10, Th8, Th7;
hence REAL_Music is non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_tonic satisfying_commutativity satisfying_Nat satisfying_harmonic_closed MusicStruct ; :: thesis: verum