<?xml version="1.0"?>
<div><span class="kw">theorem </span><a NAME="T100"><span class="comment"><font color="firebrick">:: SRINGS_5:100</font></span><br/></a><div class="add"> <a href="euclid.html#K13" title="EUCLID:func.13">Pitag_dist</a> 1 <a href="binop_1.html#R8" title="BINOP_1:pred.8">=</a>  <a href="srings_5.html#K25" title="SRINGS_5:func.25">Infty_dist</a> 1</div></div>
