<![CDATA[
\input utility.tdf
\input common.tdf
\input geom.tdf
\lineb
\centerline{\bigrm{ Small Geometry Example}}
\lineb
\lineb
%
%undefined_term: \Point
%undefined_term: \Line
%set_precedence \times 6
%undefined_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
\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
\note 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
\note 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
\note 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
\note 13 $(A,B,\ne,\in\Point)$ \By .10
\note 14 $\One z \in \Line(A \times z \And B \times z)$ \By 1.2;.13
\lineb We have
\note 15 $(L = \The z \in \Line(A \times z \And B \times z))$ \By .14, .8
\note 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
\note 17 $(x = L)$ \By .16;.11
\note 18 $(y = L)$ \By .16;.12
\note 19 $(x = y)$ \By .17,.18
\lineb This is a contradiction.
\note 20 $\false$ \By .3,.19
\lineb Hence
\note 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
]]>