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

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