thus |.+infty.| = +infty by Def1; :: thesis: |.-infty.| = +infty
- -infty = +infty by XXREAL_3:23;
hence |.-infty.| = +infty by Def1; :: thesis: verum