let x be ext-real negative non real number ; :: thesis: x = -infty
not x in REAL ;
hence x = -infty by XXREAL_0:14; :: thesis: verum