Book XI · Proposition 10

XI.10

If two straight lines meeting one another be parallel to two straight lines meeting one another not in the same plane, they will contain equal angles.Heath, 1908

Every step, checked

• the arms are not in one planegiven
• neither pair is in a straight linegiven
• the arms are parallel, each to eachby XI.Def.8
• so the angles they contain are equalby XI.10

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

Nothing. It draws no intersections and reads nothing off the picture.

The proposition as code

@proposition(
    "XI.10",
    THEOREM,
    sample=samples3.tetrahedron,
)
def prop_XI_10(o: Point3, a: Point3, b: Point3, c: Point3) -> Out:
    """Two lines meeting, parallel to two others meeting elsewhere, contain
    equal angles."""
    hypothesis("the arms are not in one plane", not coplanar(o, a, b, c))
    hypothesis("neither pair is in a straight line",
               not collinear3(o, a, b))
    # The second pair is the first carried over to another point, so the arms
    # really are parallel: that is the hypothesis, and building it is how the
    # figure gets one that satisfies it.
    step = vector_between(o, c)
    away = posit3(Point3(o.x + step[0], o.y + step[1], o.z + step[2]), "D")
    far_a = posit3(Point3(a.x + step[0], a.y + step[1], a.z + step[2]), "E")
    far_b = posit3(Point3(b.x + step[0], b.y + step[1], b.z + step[2]), "F")
    for pair in ((o, a), (o, b), (away, far_a), (away, far_b)):
        line3(*pair)

    claim("the arms are parallel, each to each", "XI.Def.8",
          _parallel3(Line3.through(o, a), Line3.through(away, far_a))
          and _parallel3(Line3.through(o, b), Line3.through(away, far_b)))
    claim("so the angles they contain are equal", "XI.10",
          angle_at3(a, o, b) == angle_at3(far_a, away, far_b))
    return Out(angles=(angle_at3(a, o, b), angle_at3(far_a, away, far_b)))