let a, b be Real; :: thesis: ( b ^2 <= a ^2 & a >= 0 implies ( - a <= b & b <= a ) )

assume that

A1: b ^2 <= a ^2 and

A2: a >= 0 ; :: thesis: ( - a <= b & b <= a )

assume that

A1: b ^2 <= a ^2 and

A2: a >= 0 ; :: thesis: ( - a <= b & b <= a )

now :: thesis: ( not - a > b & not b > a )

hence
( - a <= b & b <= a )
; :: thesis: verumassume A3:
( - a > b or b > a )
; :: thesis: contradiction

hence contradiction ; :: thesis: verum

end;hence contradiction ; :: thesis: verum