set MS = REAL_Music ;
take REAL_Music ; :: thesis: ( 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 & not REAL_Music is empty )
thus ( 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 & not REAL_Music is empty ) by Th7, Th8, Th9, Th4, Th10, Th12; :: thesis: verum