Book XI · Proposition 16

XI.16

If two parallel planes be cut by any plane, their common sections are parallel.Heath, 1908

Every step, checked

• the three points describe a planegiven
• D is off that planegiven
• the two planes are parallelgiven
• each common section is a straight lineby XI.3
• and the two sections are parallel to one anotherby XI.16

What it needs, and what needs it

Needs: XI.3

Used by: XI.24

Depth: 1 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 meet (×2)continuity
• a plane is described, and XI Def. 1-2; no postulate describes a plane (×3)solid

The proposition as code

@proposition("XI.16", THEOREM, sample=samples3.plane_and_point)
def prop_XI_16(a: Point3, b: Point3, c: Point3, d: Point3) -> Out:
    """Two parallel planes cut by a third have parallel common sections."""
    hypothesis("the three points describe a plane", not collinear3(a, b, c))
    hypothesis("D is off that plane", not coplanar(a, b, c, d))
    step = vector_between(a, d)
    first = plane_through(a, b, c, "the first plane")
    lifted = [posit3(Point3(p.x + step[0], p.y + step[1], p.z + step[2]), name)
              for p, name in zip((a, b, c), ("E", "F", "G"))]
    second = plane_through(*lifted, "the second, parallel to it")
    hypothesis("the two planes are parallel", parallel_planes(first, second))

    cutter = plane_through(a, lifted[0], b, "the cutting plane")
    here = meet_planes(first, cutter)
    there = meet_planes(second, cutter)

    claim("each common section is a straight line", "XI.3",
          isinstance(here, Line3) and isinstance(there, Line3))
    claim("and the two sections are parallel to one another", "XI.16",
          _parallel3(here, there))
    return Out(sections=(here, there))