let r, s be Real; :: thesis: ( (r ^2) + (s ^2) = 1 implies ( - 1 <= r & r <= 1 ) )
s ^2 >= 0 by XREAL_1:63;
then - (s ^2) <= - 0 ;
then (r ^2) - ((r ^2) + (s ^2)) <= 0 ;
hence ( (r ^2) + (s ^2) = 1 implies ( - 1 <= r & r <= 1 ) ) by SQUARE_1:43; :: thesis: verum