\input utility.tdf
\input common.tdf
\input geom.tdf
\lineb

\centerline{\bigrm{ Small Geometry Example}}
\lineb
\lineb

%
%primitive_term: \Point
%primitive_term: \Line
%precedence= 6 
%primitive_formula: (x \times y)


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

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

$\Point$
\lineb

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

$\Line$
\lineb

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

\noindent{}Finally 
\lineb

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

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

\lineb

\chap{1.  Postulates}

\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
	\notea 1 $(x \in \Line)$ \By G
	\notea 2 $(y \in \Line)$ \By G
	\notea 3 $(x \ne y)$ \By  G
\lineb Take the following as given and get a contradiction.
	\notea 4 $\Not\Unq z \in \Point (x \times z \And y \times z)$  \By G
\lineb It is immediate that
	\notea 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
	\notea 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 
	\notea 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 
	\notea 8 $(L \ident \The z \in \Line(A \times z \And B \times z))$ \By S 
\lineb We have then that
	\notea 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 06.1
\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


\chap{3.  Additions to  the Common Notions File}


\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

This geometry example is taken from the
book {\it Fundamental Concepts of Geometry}
by Bruce E. Meserve, Dover 1983, (page 13, Exercise 1).

%
\centerline {\bf{TABLE OF CONTENTS}}
 
\lineb
\lineb
\lineb\  1. Postulates\hfill \the\count101
\lineb\  2. Theorems\hfill \the\count102
\lineb\  3. Additional Common Notions\hfill \the\count103
\lineb

\end

