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

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

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

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

end;

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

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

end;

end;