let r be Element of R; :: thesis: ( ( a in O implies ( r = absolute_value (O,a) iff r = a ) ) & ( not a in O implies ( r = absolute_value (O,a) iff r = - a ) ) )
thus ( a in O implies ( r = absolute_value (O,a) iff r = a ) ) by defa; :: thesis: ( not a in O implies ( r = absolute_value (O,a) iff r = - a ) )
thus ( not a in O implies ( r = absolute_value (O,a) iff r = - a ) ) :: thesis: verum
proof
assume AS: not a in O ; :: thesis: ( r = absolute_value (O,a) iff r = - a )
O \/ (- O) = the carrier of R by REALALG1:def 8;
then a in - O by AS, XBOOLE_0:def 3;
hence ( r = absolute_value (O,a) iff r = - a ) by defa; :: thesis: verum
end;