a1:
StoppingSet T c= ExtREAL
by XXREAL_0:def 4, XBOOLE_0:def 3;

{+infty} c= ExtREAL by ZFMISC_1:31;

hence (StoppingSet T) \/ {+infty} is Subset of ExtREAL by a1, XBOOLE_1:8; :: thesis: verum

{+infty} c= ExtREAL by ZFMISC_1:31;

hence (StoppingSet T) \/ {+infty} is Subset of ExtREAL by a1, XBOOLE_1:8; :: thesis: verum