thus ( not -infty is integer & -infty <> +infty ) ; :: according to FVALUAT1:def 1 :: thesis: verum