<?xml version="1.0"?>
<div><span class="kw">theorem </span><a NAME="T25"><span class="comment"><font color="firebrick">:: GLIBPRE1:25</font></span><br/></a><div class="add"> for <font color="Olive" title="b1">G</font> being   <a href="glib_000.html#NM2" title="GLIB_000:NM.2">_Graph</a>  st (  for <font color="Olive" title="b2">v</font> being   <a href="glib_000.html#NM10" title="GLIB_000:NM.10">Vertex</a> of <font color="Olive" title="b1">G</font>  holds <br/>( <font color="Olive" title="b2">v</font> <a href="glib_000.html#K36" title="GLIB_000:func.36">.inNeighbors()</a>  <a href="tarski.html#R1" title="TARSKI:pred.1">c=</a> <span class="p1">(<span class="default"><a href="glib_000.html#K6" title="GLIB_000:func.6">the_Vertices_of</a> <font color="Olive" title="b1">G</font></span>)</span> <a href="subset_1.html#K6" title="SUBSET_1:func.6">\</a> <span class="p1"><a href="domain_1.html#K6" title="DOMAIN_1:func.6">{</a><span class="default"><font color="Olive" title="b2">v</font></span><a href="domain_1.html#K6" title="DOMAIN_1:func.6">}</a></span> or <font color="Olive" title="b2">v</font> <a href="glib_000.html#K37" title="GLIB_000:func.37">.outNeighbors()</a>  <a href="tarski.html#R1" title="TARSKI:pred.1">c=</a> <span class="p1">(<span class="default"><a href="glib_000.html#K6" title="GLIB_000:func.6">the_Vertices_of</a> <font color="Olive" title="b1">G</font></span>)</span> <a href="subset_1.html#K6" title="SUBSET_1:func.6">\</a> <span class="p1"><a href="domain_1.html#K6" title="DOMAIN_1:func.6">{</a><span class="default"><font color="Olive" title="b2">v</font></span><a href="domain_1.html#K6" title="DOMAIN_1:func.6">}</a></span> or <font color="Olive" title="b2">v</font> <a href="glib_000.html#K38" title="GLIB_000:func.38">.allNeighbors()</a>  <a href="tarski.html#R1" title="TARSKI:pred.1">c=</a> <span class="p1">(<span class="default"><a href="glib_000.html#K6" title="GLIB_000:func.6">the_Vertices_of</a> <font color="Olive" title="b1">G</font></span>)</span> <a href="subset_1.html#K6" title="SUBSET_1:func.6">\</a> <span class="p1"><a href="domain_1.html#K6" title="DOMAIN_1:func.6">{</a><span class="default"><font color="Olive" title="b2">v</font></span><a href="domain_1.html#K6" title="DOMAIN_1:func.6">}</a></span> ) ) holds <br/><font color="Olive" title="b1">G</font> is  <a href="glib_000.html#V3" title="GLIB_000:attr.3">loopless</a> </div></div>
