let r, s be real number ; :: thesis: ( (abs r) + (abs s) = 0 implies r = 0 )
assume A1: (abs r) + (abs s) = 0 ; :: thesis: r = 0
set aa = abs r;
set ab = abs s;
A2: ( 0 <= abs r & 0 <= abs s ) by COMPLEX1:132;
abs r = - (abs s) by A1;
then abs r = 0 by A2;
hence r = 0 by ABSVALUE:7; :: thesis: verum