theorem Th92: :: MUSIC_S1:115

for HPS being Heptatonic_Pythagorean_Score
for frequency being Element of HPS holds
( 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 )