let a, b be Real; :: thesis: |.a.| <= sqrt ((a ^2) + (b ^2))
( a ^2 >= 0 & (a ^2) + 0 <= (a ^2) + (b ^2) ) by XREAL_1:6, XREAL_1:63;
then sqrt (a ^2) <= sqrt ((a ^2) + (b ^2)) by SQUARE_1:26;
hence |.a.| <= sqrt ((a ^2) + (b ^2)) by Lm28; :: thesis: verum