let z be Quaternion; :: thesis: Im2 z <= |.z.|
0 <= (Im2 z) ^2 by XREAL_1:63;
then A1: sqrt ((Im2 z) ^2) <= sqrt (((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2)) by Lm27, SQUARE_1:26;

per cases ( Im2 z >= 0 or Im2 z < 0 ) ;

suppose Im2 z >= 0 ; :: thesis: Im2 z <= |.z.|

hence Im2 z <= |.z.| by A1, SQUARE_1:22; :: thesis: verum

end;

suppose A2: Im2 z < 0 ; :: thesis: Im2 z <= |.z.|

then - (Im2 z) <= |.z.| by A1, SQUARE_1:23;
hence Im2 z <= |.z.| by A2; :: thesis: verum

end;

end;