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