set F = the sequence of ExtREAL;
reconsider A = rng the sequence of ExtREAL as non empty Subset of ExtREAL ;
take A ; :: thesis: A is V85()
assume not A is empty ; :: according to SUPINF_2:def 8 :: thesis: ex F being sequence of ExtREAL st A = rng F
thus ex F being sequence of ExtREAL st A = rng F ; :: thesis: verum