<?xml version="1.0"?>
<div><div><a NAME="S5"><span class="kw">scheme  </span><span class="comment"><font color="firebrick">:: NAT_1:sch 5</font></span><br/></a><span class="lab"><font color="Green" title="E5">Min</font></span>{ <font color="Maroon">P<sub>1</sub></font>[  <a href="nat_1.html#NM1" title="NAT_1:NM.1">Nat</a>] } :<br/><div class="add"><a NAME="E2:22"/>
 ex <font color="Olive" title="b1">k</font> being   <a href="nat_1.html#NM1" title="NAT_1:NM.1">Nat</a> st <br/>( <font color="Maroon">P<sub>1</sub></font>[<font color="Olive" title="b1">k</font>] &amp; (  for <font color="Olive" title="b2">n</font> being   <a href="nat_1.html#NM1" title="NAT_1:NM.1">Nat</a>  st <font color="Maroon">P<sub>1</sub></font>[<font color="Olive" title="b2">n</font>] holds <br/><font color="Olive" title="b1">k</font> <a href="xxreal_0.html#R1" title="XXREAL_0:pred.1">&lt;=</a> <font color="Olive" title="b2">n</font> ) )
 </div><span class="kw">provided</span><div class="add"><a NAME="E1:22"/><span class="lab"><font color="Green" title="E8">A1</font></span>: 
 ex <font color="Olive" title="b1">k</font> being   <a href="nat_1.html#NM1" title="NAT_1:NM.1">Nat</a> st <font color="Maroon">P<sub>1</sub></font>[<font color="Olive" title="b1">k</font>]
 </div></div></div>
