Book XI · Proposition 2

XI.2

If two straight lines cut one another, they are in one plane, and every triangle is in one plane.Heath, 1908

Also unsound in Euclid: the proof assumes the very thing about planes that XI.1 was meant to establish.

Every step, checked

• the two straight lines cut one another at Ogiven
• the two lines lie in one planeby XI.Def.7
• and so does the whole triangle they makeby XI.2
• the plane is the only one holding all three, being determined by themby XI.Def.7

What it needs, and what needs it

Needs: nothing earlier.

Rests on: XI.Def.7

Depth: 0 steps of argument above the first principles. Parallel postulate: not needed.

What it takes on trust

• a plane is described, and XI Def. 1-2; no postulate describes a plane (×2)solid

The proposition as code

@proposition(
    "XI.2",
    THEOREM,
    sample=samples3.cutting_lines,
    note="Also unsound in Euclid: the proof assumes the very thing about planes "
    "that XI.1 was meant to establish.",
)
def prop_XI_2(o: Point3, a: Point3, b: Point3) -> Out:
    """Two straight lines that cut one another are in one plane."""
    # Euclid's own condition -- "if two straight lines cut one another" -- and
    # not a guard of ours: two lines through O are one line exactly when the
    # three points are in a straight line.
    hypothesis("the two straight lines cut one another at O",
               not collinear3(o, a, b))
    surface = plane_through(o, a, b, "their plane")
    line3(o, a)
    line3(o, b)
    line3(a, b, "the triangle is closed")

    claim("the two lines lie in one plane", "XI.Def.7",
          on_plane(o, surface) and on_plane(a, surface) and on_plane(b, surface))
    claim("and so does the whole triangle they make", "XI.2",
          all(on_plane(Point3(a.x + (b.x - a.x) * Fraction(k, 4),
                              a.y + (b.y - a.y) * Fraction(k, 4),
                              a.z + (b.z - a.z) * Fraction(k, 4)), surface)
              for k in range(5)))
    claim("the plane is the only one holding all three, being determined by them",
          "XI.Def.7", plane_through(o, a, b) == surface)
    return Out(plane=surface)