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

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

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

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

end;

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

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

end;

end;