let S be non empty satisfying_Real MusicStruct ; :: thesis: ( S is satisfying_euclidean implies S is satisfying_interval )
assume A1: S is satisfying_euclidean ; :: thesis: S is satisfying_interval

now :: thesis: for f1, f2, f3 being Element of S st the Ratio of S . (f1,f2) = the Ratio of S . (f1,f3) holds
f2 = f3

let f1, f2, f3 be Element of S; :: thesis: ( the Ratio of S . (f1,f2) = the Ratio of S . (f1,f3) implies f2 = f3 )
assume the Ratio of S . (f1,f2) = the Ratio of S . (f1,f3) ; :: thesis: f2 = f3
then (@ f2) / (@ f1) = the Ratio of S . (f1,f3) by A1;
then (@ f2) / (@ f1) = (@ f3) / (@ f1) by A1;
hence f2 = f3 by XCMPLX_1:53; :: thesis: verum

end;

hence S is satisfying_interval ; :: thesis: verum