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