let r be quaternion number ; :: thesis: ( r <> 0 implies |.r.| > 0 )
assume r <> 0 ; :: thesis: |.r.| > 0
then |.r.| <> 0 by Lm3;
hence |.r.| > 0 by QUATERNI:67; :: thesis: verum