let a, b be Real; ( b ^2 < a ^2 & a >= 0 implies ( - a < b & b < a ) )
assume that
A1:
b ^2 < a ^2
and
A2:
a >= 0
; ( - a < b & b < a )
now ( not - a >= b & not b >= a )assume A3:
(
- a >= b or
b >= a )
;
contradictionnow ( ( - a >= b & contradiction ) or ( b >= a & contradiction ) )end; hence
contradiction
;
verum end;
hence
( - a < b & b < a )
; verum