let x be ext-real negative non real number ; :: thesis: x = -infty
( not x in REAL & x <> +infty ) ;
hence x = -infty by XXREAL_0:14; :: thesis: verum