thus |.+infty.| = +infty by EXTREAL1:3; :: thesis: |.-infty.| = +infty
- -infty = +infty by XXREAL_3:23;
hence |.-infty.| = +infty by EXTREAL1:4; :: thesis: verum