theorem Th12: :: MUSIC_S1:14
for f1, f2, f3, f4 being Element of REAL_Music holds
( the Ratio of REAL_Music . (f1,f2) = the Ratio of REAL_Music . (f3,f4) iff the Ratio of REAL_Music . (f2,f1) = the Ratio of REAL_Music . (f4,f3) )