let r, s be real number ; :: thesis: ( not abs r = abs s or r = s or r = - s )
assume A1: abs r = abs s ; :: thesis: ( r = s or r = - s )
assume A2: r <> s ; :: thesis: r = - s

per cases ( ( abs r = r & abs s = s ) or ( abs r = r & abs s = - s ) or ( abs r = - r & abs s = s ) or ( abs r = - r & abs s = - s ) ) by Def1;

suppose ( abs r = r & abs s = s ) ; :: thesis: r = - s

hence r = - s by A1, A2; :: thesis: verum

end;

suppose ( abs r = r & abs s = - s ) ; :: thesis: r = - s

hence r = - s by A1; :: thesis: verum

end;

suppose ( abs r = - r & abs s = s ) ; :: thesis: r = - s

hence r = - s by A1; :: thesis: verum

end;

suppose ( abs r = - r & abs s = - s ) ; :: thesis: r = - s

hence r = - s by A1, A2; :: thesis: verum

end;

end;