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