Book XI · Proposition 3

XI.3

If two planes cut one another, their common section is a straight line.Heath, 1908

The one Euclid proves rather than assumes, which is why the kernel records a call to it as a step and not as a primitive.

Every step, checked

• the four points are not in one planegiven
• the two planes are not one planegiven
• the common section is a straight lineby XI.3
• and every point of it lies in both planesby XI.3
• the two points the planes share lie on itby XI.3

What it needs, and what needs it

Needs: nothing earlier.

Used by: XI.16 XI.19 XI.28 XI.38

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

What it takes on trust

• a plane-plane intersection is used, though no postulate asserts that two planes meetcontinuity
• a plane is described, and XI Def. 1-2; no postulate describes a plane (×2)solid

The proposition as code

@proposition(
    "XI.3",
    THEOREM,
    sample=samples3.four_in_space,
    note="The one Euclid proves rather than assumes, which is why the kernel "
    "records a call to it as a step and not as a primitive.",
)
def prop_XI_3(a: Point3, b: Point3, c: Point3, d: Point3) -> Out:
    """If two planes cut one another, their common section is a straight line."""
    hypothesis("the four points are not in one plane", not coplanar(a, b, c, d))
    first = plane_through(a, b, c, "the first plane")
    second = plane_through(a, b, d, "the second")
    hypothesis("the two planes are not one plane", first != second)

    section = meet_planes(first, second)
    claim("the common section is a straight line", "XI.3",
          isinstance(section, Line3))
    claim("and every point of it lies in both planes", "XI.3",
          all(on_plane(section.at(Fraction(k, 3)), first)
              and on_plane(section.at(Fraction(k, 3)), second)
              for k in range(-6, 7)))
    claim("the two points the planes share lie on it", "XI.3",
          section.holds(a) and section.holds(b))
    return Out(section=section)