theorem :: EUCLID10:33

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle & angle (B,A,C) = PI / 2 holds
(angle (C,B,A)) + (angle (A,C,B)) = PI / 2