:: deftheorem Def25 defines satisfying_euclidean MUSIC_S1:def 78 :
for MS being non empty satisfying_Real MusicStruct holds
( MS is satisfying_euclidean iff for f1, f2 being Element of MS holds the Ratio of MS . (f1,f2) = (@ f2) / (@ f1) );