let a be real number ; :: thesis: ( |.a.| = a or |.a.| = - a )
( a >= 0 or a < 0 ) ;
hence ( |.a.| = a or |.a.| = - a ) by Lm23, Th129; :: thesis: verum