-infty <> +infty by TARSKI:def 2, Lm1;
hence -infty < +infty by Def5, Lm4, Lm6; :: thesis: verum