let J be ExtREAL_sequence; :: thesis: ( not J is without-infty or sup (rng J) in REAL or sup (rng J) = +infty )
assume A1: J is without-infty ; :: thesis: ( sup (rng J) in REAL or sup (rng J) = +infty )
dom J = NAT by FUNCT_2:def 1;
then ( J . 1 in rng J & -infty < J . 1 ) by A1, Def5, FUNCT_1:12;
then -infty is not UpperBound of rng J by 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