:: deftheorem Def13a defines satisfying_harmonic_closed MUSIC_S1:def 18 :
for S being MusicStruct holds
( S is satisfying_harmonic_closed iff for frequency being Element of S
for n being non zero Nat ex harmonique being Element of S st [frequency,harmonique] in Class ( the Equidistance of S,[1,n]) );