let J be ExtREAL_sequence; :: thesis: ( not J is () or sup (rng J) in REAL or sup (rng J) = +infty )
assume J is () ; :: thesis: ( sup (rng J) in REAL or sup (rng J) = +infty )
then A1: -infty < J . 1 ;
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