let a be Real; :: thesis: ( a <= 0 implies |.a.| = - a )
assume a <= 0 ; :: thesis: |.a.| = - a
then |.(- a).| = - a by Th43;
hence |.a.| = - a by Lm26; :: thesis: verum