let r, s be Real; :: thesis: ( not |.r.| = |.s.| or r = s or r = - s )
assume A1: |.r.| = |.s.| ; :: thesis: ( r = s or r = - s )
assume A2: r <> s ; :: thesis: r = - s
per cases ( ( |.r.| = r & |.s.| = s ) or ( |.r.| = r & |.s.| = - s ) or ( |.r.| = - r & |.s.| = s ) or ( |.r.| = - r & |.s.| = - s ) ) by Def1;
suppose ( |.r.| = r & |.s.| = s ) ; :: thesis: r = - s
hence r = - s by A1, A2; :: thesis: verum
end;
suppose ( |.r.| = r & |.s.| = - s ) ; :: thesis: r = - s
hence r = - s by A1; :: thesis: verum
end;
suppose ( |.r.| = - r & |.s.| = s ) ; :: thesis: r = - s
hence r = - s by A1; :: thesis: verum
end;
suppose ( |.r.| = - r & |.s.| = - s ) ; :: thesis: r = - s
hence r = - s by A1, A2; :: thesis: verum
end;
end;