-infty <> +infty by TARSKI:def 2;
hence -infty < +infty by Def5, Lm3, Lm5; :: thesis: verum