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