Book XI · Proposition 21

XI.21

Any solid angle is contained by plane angles less than four right angles.Heath, 1908

Every step, checked

What it needs, and what needs it

Needs: nothing earlier.

Used by: XIII.18

Rests on: XI.Def.11

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.21", THEOREM, sample=samples3.tetrahedron)
def prop_XI_21(o: Point3, a: Point3, b: Point3, c: Point3) -> Out:
    """Any solid angle is contained by plane angles less than four right angles."""
    hypothesis("the solid angle is a genuine one", not coplanar(o, a, b, c),
               guard=True)
    for arm in (a, b, c):
        line3(o, arm)

    first, second, third = angle_at3(a, o, b), angle_at3(b, o, c), angle_at3(a, o, c)
    claim("each plane angle is less than two right angles", "XI.Def.11",
          all(sign(angle.cos + 1) > 0 for angle in (first, second, third)))
    claim("and the three together are less than four right angles", "XI.21",
          _under_four_right_angles(first, second, third)
          and _under_four_right_angles(second, third, first)
          and _under_four_right_angles(first, third, second))
    return Out(angles=(first, second, third))