let A, B, C be Point of (TOP-REAL 2); :: thesis: ( A,B,C is_a_triangle & angle (B,A,C) = PI / 2 implies (angle (C,B,A)) + (angle (A,C,B)) = PI / 2 )
assume that
A1: A,B,C is_a_triangle and
A2: angle (B,A,C) = PI / 2 ; :: thesis: (angle (C,B,A)) + (angle (A,C,B)) = PI / 2
A3: A,B,C are_mutually_distinct by A1, EUCLID_6:20;
((angle (B,A,C)) + (angle (A,C,B))) + (angle (C,B,A)) = PI by A2, COMPTRIG:5, A3, EUCLID_3:47;
hence (angle (C,B,A)) + (angle (A,C,B)) = PI / 2 by A2; :: thesis: verum