<?xml version="1.0"?>
<div><span class="kw">theorem </span><a NAME="T10"><span class="comment"><font color="firebrick">:: MUSIC_S1:10</font></span><br/></a><div class="add"> <a href="nat_lat.html#K6" title="NAT_LAT:func.6">NATPLUS</a>  <a href="tarski.html#R1" title="TARSKI:pred.1">c=</a>  the <a href="struct_0.html#U1" title="STRUCT_0:sel.1">carrier</a> of <a href="music_s1.html#K6" title="MUSIC_S1:func.6">REAL_Music</a> <span class="kw">by</span> <span class="lab"><a class="ref" href="music_s1.html#T5" target="_self" onmouseover="rs('music_s1/T5')" onmouseout="rh()">Th4</a></span>;<br/></div></div>
