Book XI · Proposition 7

XI.7

If two straight lines be parallel and points be taken at random on each of them, the straight line joining the points is in the same plane with the parallel straight lines.Heath, 1908

Every step, checked

• the two lines are parallelgiven
• they are two lines and not onegiven
• both parallels lie in the one planeby XI.Def.8
• and the joining line lies in it throughoutby XI.7

What it needs, and what needs it

Needs: nothing earlier.

Rests on: XI.Def.8

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 planesolid

The proposition as code

@proposition(
    "XI.7",
    THEOREM,
    sample=samples3.parallel_lines3,
)
def prop_XI_7(a: Point3, b: Point3, c: Point3, d: Point3) -> Out:
    """The line joining points on two parallels is in their plane."""
    first, second = Line3.through(a, b), Line3.through(c, d)
    hypothesis("the two lines are parallel", _parallel3(first, second))
    hypothesis("they are two lines and not one", not first.holds(c))
    surface = plane_through(a, b, c, "the plane of the parallels")
    line3(a, b)
    line3(c, d)
    joining = line3(a, c, "the joining line")

    claim("both parallels lie in the one plane", "XI.Def.8",
          on_plane(a, surface) and on_plane(b, surface)
          and on_plane(c, surface) and on_plane(d, surface))
    claim("and the joining line lies in it throughout", "XI.7",
          all(on_plane(joining.at(Fraction(k, 4)), surface) for k in range(-8, 9)))
    return Out(plane=surface, joining=joining)