<?xml version="1.0"?>
<div><span class="kw">theorem </span><span class="lab"><font color="Green" title="E14">Th12</font></span>: <a NAME="T15"><span class="comment"><font color="firebrick">:: EUCLID12:15</font></span><br/></a><div class="add"> for <font color="Olive" title="b1">OO</font>, <font color="Olive" title="b2">Ox</font>, <font color="Olive" title="b3">Oy</font> being    <a href="finseq_2.html#M2" title="FINSEQ_2:mode.2">Element</a> of  <a href="euclid.html#K1" title="EUCLID:func.1">REAL</a> 2  st <font color="Olive" title="b1">OO</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> <span class="p1"><a href="euclid.html#K19" title="EUCLID:func.19">|[</a><span class="default"><a href="ordinal1.html#K5" title="ORDINAL1:func.5">0</a>,<a href="ordinal1.html#K5" title="ORDINAL1:func.5">0</a></span><a href="euclid.html#K19" title="EUCLID:func.19">]|</a></span> &amp; <font color="Olive" title="b2">Ox</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> <span class="p1"><a href="euclid.html#K19" title="EUCLID:func.19">|[</a><span class="default">1,<a href="ordinal1.html#K5" title="ORDINAL1:func.5">0</a></span><a href="euclid.html#K19" title="EUCLID:func.19">]|</a></span> &amp; <font color="Olive" title="b3">Oy</font> <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a> <span class="p1"><a href="euclid.html#K19" title="EUCLID:func.19">|[</a><span class="default"><a href="ordinal1.html#K5" title="ORDINAL1:func.5">0</a>,1</span><a href="euclid.html#K19" title="EUCLID:func.19">]|</a></span> holds <br/> <a href="euclid.html#K1" title="EUCLID:func.1">REAL</a> 2 <a href="hidden.html#R1" title="HIDDEN:pred.1">=</a>  <a href="euclidlp.html#K4" title="EUCLIDLP:func.4">plane</a> (<font color="Olive" title="b1">OO</font>,<font color="Olive" title="b2">Ox</font>,<font color="Olive" title="b3">Oy</font>)</div></div>
