let MS be satisfying_equiv satisfying_interval satisfying_tonic satisfying_Nat satisfying_harmonic_closed satisfying_harmonique_stable MusicStruct ; :: thesis: for a, b being Element of MS holds a,a equiv b,b
let a, b be Element of MS; :: thesis: a,a equiv b,b
( 1 -harmonique (MS,a) = a & 1 -harmonique (MS,b) = b ) by Th40;
hence a,a equiv b,b by Def10; :: thesis: verum