let a be Real; :: thesis: ( |.a.| = a or |.a.| = - a )
( a >= 0 or a < 0 ) ;
hence ( |.a.| = a or |.a.| = - a ) by Lm27, Th43; :: thesis: verum