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

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