let J be ExtREAL_sequence; :: thesis: ( not J is without-infty or sup (rng J) in REAL or sup (rng J) = +infty )
assume J is without-infty ; :: thesis: ( sup (rng J) in REAL or sup (rng J) = +infty )
then A1: -infty < J . 1 by Def5;
dom J = NAT by FUNCT_2:def 1;
then -infty is not UpperBound of rng J by A1, FUNCT_1:3, XXREAL_2:def 1;
then sup (rng J) <> -infty by XXREAL_2:def 3;
hence ( sup (rng J) in REAL or sup (rng J) = +infty ) by XXREAL_0:14; :: thesis: verum