take REAL_Music ; :: thesis: REAL_Music is classical_fifth
thus REAL_Music is classical_fifth by Th38; :: thesis: verum