<?xml version="1.0"?>
<div class="add">

<b>let </b><font color="Maroon">c<sub>1</sub></font> be   <a href="trees_2.html#NM4">DecoratedTree</a>;<br/><b>let </b><font color="Maroon">c<sub>2</sub></font> be   <a href="trees_4.html#NM1">Node</a> of <font color="Maroon">c<sub>1</sub></font>;<br/>



<a NAME="E1:14"/>
( ( <font color="Maroon">c<sub>1</sub></font> <a href="trees_2.html#K5">|</a> <font color="Maroon">c<sub>2</sub></font> is <a href="trees_9.html#V1" target="_self">root</a> implies  <a href="relat_1.html#K1">dom</a> <span class="p1">(<span class="default"><font color="Maroon">c<sub>1</sub></font> <a href="trees_2.html#K5">|</a> <font color="Maroon">c<sub>2</sub></font></span>)</span> <a href="hidden.html#R1">=</a>  <a href="trees_1.html#K2">elementary_tree</a> 0 ) &amp; (  <a href="relat_1.html#K1">dom</a> <span class="p1">(<span class="default"><font color="Maroon">c<sub>1</sub></font> <a href="trees_2.html#K5">|</a> <font color="Maroon">c<sub>2</sub></font></span>)</span> <a href="hidden.html#R1">=</a>  <a href="trees_1.html#K2">elementary_tree</a> 0 implies <font color="Maroon">c<sub>1</sub></font> <a href="trees_2.html#K5">|</a> <font color="Maroon">c<sub>2</sub></font> is <a href="trees_9.html#V1" target="_self">root</a> ) &amp;  <a href="relat_1.html#K1">dom</a> <span class="p1">(<span class="default"><font color="Maroon">c<sub>1</sub></font> <a href="trees_2.html#K5">|</a> <font color="Maroon">c<sub>2</sub></font></span>)</span> <a href="hidden.html#R1">=</a> <span class="p1">(<span class="default"><a href="relat_1.html#K1">dom</a> <font color="Maroon">c<sub>1</sub></font></span>)</span> <a href="trees_1.html#K4">|</a> <font color="Maroon">c<sub>2</sub></font> &amp; ( <font color="Maroon">c<sub>2</sub></font> <a href="hidden.html#R2">in</a>  <a href="trees_1.html#K3">Leaves</a> <span class="p1">(<span class="default"><a href="relat_1.html#K1">dom</a> <font color="Maroon">c<sub>1</sub></font></span>)</span> implies <span class="p1">(<span class="default"><a href="relat_1.html#K1">dom</a> <font color="Maroon">c<sub>1</sub></font></span>)</span> <a href="trees_1.html#K4">|</a> <font color="Maroon">c<sub>2</sub></font> <a href="hidden.html#R1">=</a>  <a href="trees_1.html#K2">elementary_tree</a> 0 ) &amp; ( <span class="p1">(<span class="default"><a href="relat_1.html#K1">dom</a> <font color="Maroon">c<sub>1</sub></font></span>)</span> <a href="trees_1.html#K4">|</a> <font color="Maroon">c<sub>2</sub></font> <a href="hidden.html#R1">=</a>  <a href="trees_1.html#K2">elementary_tree</a> 0 implies <font color="Maroon">c<sub>2</sub></font> <a href="hidden.html#R2">in</a>  <a href="trees_1.html#K3">Leaves</a> <span class="p1">(<span class="default"><a href="relat_1.html#K1">dom</a> <font color="Maroon">c<sub>1</sub></font></span>)</span> ) )
 
<b>by </b><i><a class="ref" href="trees_9.html#D1" target="_self">Def1</a>, <a class="ref" href="trees_9.html#T5" target="_self">Th5</a>, <a class="ref" href="trees_2.html#D11">TREES_2:def 11</a></i>;<br/>
<b>hence </b><a NAME="E2:14"/>
( <font color="Maroon">c<sub>1</sub></font> <a href="trees_2.html#K5">|</a> <font color="Maroon">c<sub>2</sub></font> is <a href="trees_9.html#V1" target="_self">root</a> iff <font color="Maroon">c<sub>2</sub></font> <a href="hidden.html#R2">in</a>  <a href="trees_1.html#K3">Leaves</a> <span class="p1">(<span class="default"><a href="relat_1.html#K1">dom</a> <font color="Maroon">c<sub>1</sub></font></span>)</span> )
 ;<br/>


</div>
