let HPS be satisfying_euclidean Heptatonic_Pythagorean_Score; :: thesis: for f1, f2 being Element of HPS holds intrval (f1,f2) = the Ratio of HPS . (f1,f2)
let f1, f2 be Element of HPS; :: thesis: intrval (f1,f2) = the Ratio of HPS . (f1,f2)
the Ratio of HPS . (f1,f2) = (@ f2) / (@ f1) by Def25;
hence intrval (f1,f2) = the Ratio of HPS . (f1,f2) by Def21; :: thesis: verum