let x be Real; :: 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 Th61;
hence absreal . (- x) = absreal . x by A1, Th62; :: thesis: verum

end;

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

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

end;

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

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

end;

end;