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