Lemma·L31
Two distinct lines meet in at most one point
Lines cannot cross twice.
In every affine plane
: if
with
, then there are no two distinct points lying on both, i.e.
In words
If l and m are lines and they differ, then for any points p and q, if p lies on both lines and q lies on both lines, then p and q are the same point: two different lines meet once or not at all.
Never needed: F11 · F12 · F13 · F14 · A01 · A03 · A04 · A05 · A06 · A07 · A08 (computed from the citation graph, not asserted).
Proof
- 1Let and suppose with (D008: both points lie on and on ).
- 2Axiom (AP1) of D041 says two distinct points lie on exactly one common line. Both and are lines containing and , so the uniqueness clause of the quantifier (existential with uniqueness, unfolded via F05 and F09) forces .
- 3This contradicts (negation). Hence no such pair of points exists, and any are equal (excluded middle).
∎
Remarks
The first and most used fact of incidence geometry, and the mirror image of (AP1): two points determine one line, so two lines determine at most one point. In the projective completion, "at most one" becomes "exactly one", with parallel lines meeting at their shared point at infinity; the parallel classes are what get adjoined.