In this development of a mini-geometry, elementary set theory and arithmetic are presumed. It begins with two primitive terms and one primitive formula. The set of all points, Point, is one primitive term and the set of all lines, Line, is the other. The primitive formula, written here as (a x b), means that a and b intersect.
The first postulate (not used in the proof) uses the notation #A for the cardinality of a set A. It says that there are just three points. The second postulate uses a special quantifier, with a dot, to assert the existence of exactly one object. It also uses some special plural notation (x,y,z,∈ A) to mean (x ∈ A) and (y ∈ A) and (z ∈ A). The further modification (x,y,z,≠,∈ A) means that in addition (x ≠ y),(y ≠ z),and (x ≠ z). Hence the second postulates asserts that for any two distinct points there is exactly one line which intersects both of them.
Theorem 2.1 uses an at most one quantifier to assert that there is at most one point intersected by the two distinct points given in the hypothesis.
Notes 1, 2, and 3 restate the hypothesis as givens. Note 4 is taken as a given in order to obtain a proof by contradiction. Note 5 follows immediately from Note 4. Notes 6 and 7 give names to the two points whose existence is asserted by Note 5. Note 8 defines the line whose existence is asserted by Postulate 1.2, a fact arrived at in Note 15. But then from Notes 17 and 18 we get in Note 19 that (x = y) which is a contradiction. The notation in Note 20 is just the Boolean constant for falsehood. The fact that Note 4 has led to a contradiction gives us Note 21 which is the conclusion of the theorem.
This example is taken from the book Fundamental Concepts of Geometry by Bruce E. Meserve, Dover 1983, (page 13, Exercise 1).