let MS be satisfying_equiv satisfying_interval satisfying_tonic satisfying_Nat satisfying_harmonic_closed satisfying_harmonique_stable MusicStruct ; for a, b being Element of MS holds a,a equiv b,b
let a, b be Element of MS; 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; verum