let MS be MusicSpace; :: thesis: for f1, f2 being Element of MS ex r1, r2 being Element of REALPLUS st intrval (f1,f2) = REAL_ratio (r1,r2)
let f1, f2 be Element of MS; :: thesis: ex r1, r2 being Element of REALPLUS st intrval (f1,f2) = REAL_ratio (r1,r2)
the carrier of MS c= REALPLUS by Def07a;
then reconsider r1 = f1, r2 = f2 as Element of REALPLUS ;
consider r, s being positive Real such that
A1: ( r1 = r & r2 = s & REAL_ratio (r1,r2) = s / r ) by Def01;
( intrval (f1,f2) = s / r & REAL_ratio (r1,r2) = s / r ) by A1, Def21;
hence ex r1, r2 being Element of REALPLUS st intrval (f1,f2) = REAL_ratio (r1,r2) ; :: thesis: verum