( RAT_Music is satisfying_harmonic_closed & RAT_Music is satisfying_Nat & RAT_Music is satisfying_commutativity & RAT_Music is satisfying_tonic & RAT_Music is satisfying_interval & RAT_Music is satisfying_equiv & RAT_Music is satisfying_Real ) by Th14, Th16, Th3, Th19, Th17, Th15;
hence RAT_Music is non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_tonic satisfying_commutativity satisfying_Nat satisfying_harmonic_closed MusicStruct ; :: thesis: verum