\input utility.tdf
\input common.tdf
\input template.tdf
\lineb

\centerline{\bigrm{ Title Here}}
\lineb
\lineb

% Do you have primitive terms of formulas?
% If so put them here:
%primitive_term: \Point
%primitive_formula: \Line
% Any new infix operators need their precedence specified first:
%precedence= 6 
%primitive_formula: (x \times y)


\noindent{}{\bf {Primitive Terms}}

\noindent{}The set of all points is: 
\lineb

$\Point$
\lineb

\noindent{}{\bf {Primitive Formula}}

\noindent{}Finally 
\lineb

`$(x \times y)$'
\lineb

\noindent{}means that $x$ and $y$ cross, or are incident.  
\lineb

\lineb

% Definitions of new terms and formulas may be placed
% anywhere so long as the first usage of the new expression
% is on the left side of the definition
% 
\chap{1.  Definitions,  Theorems, Axioms}

\prop 1.1 $(\num \Point = 3)$
\lineb

The number of points is 3.
\lineb



\prop 1.2 $(x,y,\ne,\in\Point \c \One z \in \Line(x \times z \and y \times z))$
\lineb

If $x$ and $y$ are distinct points then there is exactly one line $z$ which
is incident with both $x$ and $y$.
\lineb

\prop 1.3 $\Each x \in \Line \Some y \in \Point \Not(x \times y)$
\lineb

For every line there is a point not on the line.
\lineb

\prop 1.4 $(x,y,\ne,\in\Line\c \Some z \in \Point (x \times z \and y \times z))$
\lineb

If $x$ and $y$ are distinct lines then there is a point $z$
which is incident with both $x$ and $y$.
\lineb

\prop 1.6 $(\Point \cap \Line = \e)$
\lineb

Nothing is both a point and a line.
\lineb


\prop 1.7 $(x \times y \c y \times x)$
\lineb

If $x$ is incident with $y$ then $y$ is incident with $x$.
\lineb



\chap{2.  Theorem}

\prop 2.1 $(x,y,\ne,\in\Line\c \Unq z \in \Point (x \times z \and y \times z))$
\lineb


If $x$ and $y$ are distinct lines then there is at most one point which 
incident with both $x$ and $y$.

\vfil
\eject

\lineb Proof:  Given
	\note 1 $(x \in \Line)$ \By G
	\note 2 $(y \in \Line)$ \By G
	\note 3 $(x \ne y)$ \By  G
\lineb Take the following as given and get a contradiction.
	\note 4 $\Not\Unq z \in \Point (x \times z \and y \times z)$  \By G
\lineb It is immediate that
	\note 5 $\Some u ,v (u \in \Point \and x \times u \and y \times u \and
v \in \Point \and x \times v \and y \times v \and u \ne v)$ \By .4
\lineb We therefore set
	\note 6 $(A \ident \an u \Some v(u \in \Point \and x \times u \and
  y \times u \and v \in \Point \and x \times v \and y \times v \and u \ne v))$ \By S 
	\note 7 $(B \ident  \an v(A \in \Point \and x \times A \and 
 y \times A \and v \in \Point \and x \times v \and y \times v \and A \ne v))$ \By S 
	\note 8 $(L \ident \The z \in \Line(A \times z \and B \times z))$ \By S 
\lineb We have then that
	\note 9 $\Some v(A \in \Point \and x \times A \and 
 y \times A \and v \in \Point \and x \times v \and y \times v \and A \ne v)$ \By .5,.6 
 \Notea 10 $(A \in \Point \and x \times A \and 
 y \times A \and B \in \Point \and x \times B \and y \times B \and A \ne B)$ \By .9,.7 
 \Notea 11 $(\true$
 \linec $\c x \times A \and x \times B$ \By .10
 \linec $\c A \times x \and x \times B$ \By 1.7
 \linec $\c A \times x \and B\times x $ \By 1.7
 \linec $\c x \in \Line \and A\times x \and B \times x)$ \By .1
 \Notea 12$(\true$
 \linec $\c y  \times A \and y \times B$ \By .10
 \linec $\c A \times y \and y \times B$ \By 1.7
 \linec $\c A\times y \and B\times y$ \By 1.7
 \linec $\c y \in \Line \and A\times y \and B \times y)$ \By .2
 \Notea 13 $(A,B,\ne,\in\Point)$ \By .10
 \Notea 14 $\One z \in \Line(A \times z \and B \times z)$ \By 1.2;.13
\lineb We have
 \Notea 15 $(L = \The z \in \Line(A \times z \and B \times z))$ \By  .14, .8
 \Notea 16 $(M \in \Line \and A\times M \and B\times M$
\linec $\c M \in \Line \and A\times M \and B\times M \and \ex M$ \By 01.12
\linec $\c M=L)$ \By .15
 \Notea 17 $(x = L)$ \By .16;.11
 \Notea 18 $(y = L)$ \By .16;.12
 \Notea 19 $(x = y)$ \By .17,.18
	\lineb This is a contradiction.
 \Notea 20 $\false$ \By .3,.19
	\lineb Hence
 \Notea 21 $ \Unq z \in \Point (x \times z \and y \times z)$  \By .20 H .4 
\lineb \Bye .21 H .1,.2,.3
\lineb


\vfil
\eject

% Theorems which are referred to may be anywhere in the file.

\chap{3.  Additional Theorems Needed for Reference}


\prop 3.1 $(\num A = 3 \and x,y,\ne,\in A \c \One z(x,y,z,\ne,\in A))$

\prop 3.2 $(\num A = 3 \and x \in A \c \Some y,z (x,y,z,\ne,\in A))$

\prop 3.3 $(\num A = 3 \c \Some x,y,z (x,y,z,\ne,\in A))$

\prop 3.4 $(\num A = 3 \and x,y,z,\ne,\in A \c A = \{x,y,z\})$

\prop 3.5 $(x,y,z,\ne,\in A \and A \i \{x,y,z\}\c \num A = 3)$
\lineb
\lineb

\end

