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