\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