Book I · Proposition 13

I.13

If a straight line set up on a straight line make angles, it will make either two right angles or angles equal to two right angles.Heath, 1908

Every step, checked

• B lies between A and Cgiven
• D does not lie on ACgiven
• angle ABD together with angle DBC equals two right anglesby Def.10

What it needs, and what needs it

Needs: nothing earlier.

Used by: I.14 I.15 I.28 I.29 I.32

Rests on: Def.10

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

What it takes on trust

• the argument reads a 'between' fact off the figureorder

The proposition as code

@proposition(
    "I.13",
    THEOREM,
    sample=samples.straight_line_with_ray,
)
def prop_I_13(a: Point, b: Point, c: Point, d: Point) -> Out:
    hypothesis("B lies between A and C", between(a, b, c))
    hypothesis("D does not lie on AC", not collinear(a, b, d))
    outline(a, b, c, close=False)
    line(b, d)

    left = angle_at(a, b, d)
    right = angle_at(d, b, c)
    claim("angle ABD together with angle DBC equals two right angles", "Def.10",
          left + right == STRAIGHT)
    return Out(angles=(left, right))