reconsider MS = REAL_Music as satisfying_fourth_constructible MusicSpace by Th79;
take MS ; :: thesis: MS is classical_fourth
thus MS is classical_fourth by Th80; :: thesis: verum