let HPS be satisfying_euclidean Heptatonic_Pythagorean_Score; :: thesis: for frequency being Element of HPS holds
( [((heptatonic_pythagorean_scale (HPS,frequency)) . 5),((heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 2)] in fifth HPS & [((heptatonic_pythagorean_scale (HPS,frequency)) . 6),((heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 3)] in fifth HPS & not [((heptatonic_pythagorean_scale (HPS,frequency)) . 7),((heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 4)] in fifth HPS )
let frequency be Element of HPS; :: thesis: ( [((heptatonic_pythagorean_scale (HPS,frequency)) . 5),((heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 2)] in fifth HPS & [((heptatonic_pythagorean_scale (HPS,frequency)) . 6),((heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 3)] in fifth HPS & not [((heptatonic_pythagorean_scale (HPS,frequency)) . 7),((heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 4)] in fifth HPS )
A1: ( intrval ((hepta_4 (HPS,frequency)),(hepta_1 (HPS,(Octave (HPS,frequency))))) = 3 / 2 & intrval ((hepta_5 (HPS,frequency)),(hepta_2 (HPS,(Octave (HPS,frequency))))) = 3 / 2 & intrval ((hepta_6 (HPS,frequency)),(hepta_3 (HPS,(Octave (HPS,frequency))))) <> 3 / 2 & intrval ((hepta_octave (HPS,frequency)),(hepta_4 (HPS,(Octave (HPS,frequency))))) = 3 / 2 ) by Th92;
reconsider n2 = 2, n3 = 3 as Element of HPS by Th20;
the Ratio of HPS . (n2,n3) = (@ n3) / (@ n2) by Def25
.= 3 / 2 ;
then ( the Ratio of HPS . ((hepta_4 (HPS,frequency)),(hepta_1 (HPS,(Octave (HPS,frequency))))) = the Ratio of HPS . (n2,n3) & the Ratio of HPS . ((hepta_5 (HPS,frequency)),(hepta_2 (HPS,(Octave (HPS,frequency))))) = the Ratio of HPS . (n2,n3) & the Ratio of HPS . ((hepta_6 (HPS,frequency)),(hepta_3 (HPS,(Octave (HPS,frequency))))) <> the Ratio of HPS . (n2,n3) ) by A1, Th93;
then ( n2,n3 equiv hepta_4 (HPS,frequency), hepta_1 (HPS,(Octave (HPS,frequency))) & n2,n3 equiv hepta_5 (HPS,frequency), hepta_2 (HPS,(Octave (HPS,frequency))) & not n2,n3 equiv hepta_6 (HPS,frequency), hepta_3 (HPS,(Octave (HPS,frequency))) ) by Def08a;
hence ( [((heptatonic_pythagorean_scale (HPS,frequency)) . 5),((heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 2)] in fifth HPS & [((heptatonic_pythagorean_scale (HPS,frequency)) . 6),((heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 3)] in fifth HPS & not [((heptatonic_pythagorean_scale (HPS,frequency)) . 7),((heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 4)] in fifth HPS ) by EQREL_1:18; :: thesis: verum