let a be real number ; :: thesis: ( a <= 0 implies |.a.| = - a )
assume a <= 0 ; :: thesis: |.a.| = - a
then |.(- a).| = - a by Th129;
hence |.a.| = - a by Lm22; :: thesis: verum