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

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

let f1, f2, f3, f4 be Element of S; :: thesis: ( the Ratio of S . (f2,f1) = the Ratio of S . (f4,f3) implies the Ratio of S . (f1,f2) = the Ratio of S . (f3,f4) )
assume the Ratio of S . (f2,f1) = the Ratio of S . (f4,f3) ; :: thesis: the Ratio of S . (f1,f2) = the Ratio of S . (f3,f4)
then A2: (@ f1) / (@ f2) = the Ratio of S . (f4,f3) by A1
.= (@ f3) / (@ f4) by A1 ;
thus the Ratio of S . (f1,f2) = (@ f2) / (@ f1) by A1
.= 1 / ((@ f1) / (@ f2)) by XCMPLX_1:57
.= (@ f4) / (@ f3) by A2, XCMPLX_1:57
.= the Ratio of S . (f3,f4) by A1 ; :: thesis: verum

end;

hence S is satisfying_commutativity ; :: thesis: verum