let r, s be real number ; :: thesis: ( (r ^2 ) + (s ^2 ) = 1 implies ( - 1 <= r & r <= 1 ) )
s ^2 >= 0 by XREAL_1:65;
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:112; :: thesis: verum