let a be real number ; :: thesis: ( |.a.| = a or |.a.| = - a )

per cases ( a >= 0 or a < 0 ) ;

suppose a >= 0 ; :: thesis: ( |.a.| = a or |.a.| = - a )

hence ( |.a.| = a or |.a.| = - a ) by Th129; :: thesis: verum

end;

suppose a < 0 ; :: thesis: ( |.a.| = a or |.a.| = - a )

hence ( |.a.| = a or |.a.| = - a ) by Lm23; :: thesis: verum

end;

end;