reconsider MS = REAL_Music as satisfying_fourth_constructible MusicSpace by Th79;
A1: MS is classical_fourth by Th80;

now :: thesis: for f1, f2 being Element of REAL_Music holds the Ratio of REAL_Music . (f1,f2) = (@ f2) / (@ f1)

let f1, f2 be Element of REAL_Music; :: thesis: the Ratio of REAL_Music . (f1,f2) = (@ f2) / (@ f1)
reconsider x = [f1,f2] as Element of [:REALPLUS,REALPLUS:] ;
consider y9, z9 being Element of REALPLUS such that
A2: x = [y9,z9] and
A3: REAL_ratio . x = REAL_ratio (y9,z9) by Def02;
consider y99, z99 being Element of REALPLUS such that
A4: x = [y99,z99] and
REAL_ratio . x = REAL_ratio (y99,z99) by Def02;
consider r, s being positive Real such that
A5: ( y99 = r & s = z99 & REAL_ratio (y99,z99) = s / r ) by Def01;
A6: ( s = @ f2 & r = @ f1 ) by A5, A4, XTUPLE_0:1;
A7: ( y99 = y9 & z99 = z9 ) by A2, A4, XTUPLE_0:1;
thus the Ratio of REAL_Music . (f1,f2) = (@ f2) / (@ f1) by A7, A5, A3, BINOP_1:def 1, A6; :: thesis: verum

end;

then MS is satisfying_euclidean ;
hence ex b₁ being satisfying_fourth_constructible classical_fourth MusicSpace st b₁ is satisfying_euclidean by A1; :: thesis: verum