<?xml version="1.0"?>
<div><span class="kw">theorem </span><a NAME="T18"><span class="comment"><font color="firebrick">:: MUSIC_S1:18</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#K10" title="MUSIC_S1:func.10">RAT_Music</a> <span class="kw">by</span> <span class="lab"><a class="ref" href="music_s1.html#T4" target="_self" onmouseover="rs('music_s1/T4')" onmouseout="rh()">Th3</a></span>;<br/></div></div>
