let x be real number ; :: thesis: absreal . (- x) = absreal . x

per cases ( x < 0 or 0 < x or x = 0 ) ;

suppose A1: x < 0 ; :: thesis: absreal . (- x) = absreal . x

then absreal . (- x) = - x by Th49;
hence absreal . (- x) = absreal . x by A1, Th50; :: thesis: verum

end;

suppose A2: 0 < x ; :: thesis: absreal . (- x) = absreal . x

then absreal . (- x) = - (- x) by Th50
.= x ;
hence absreal . (- x) = absreal . x by A2, Th49; :: thesis: verum

end;

suppose x = 0 ; :: thesis: absreal . (- x) = absreal . x

hence absreal . (- x) = absreal . x ; :: thesis: verum

end;

end;