now :: thesis: for x being object st x in NAT \/ {+infty} holds
x in ExtREAL

let x be object ; :: thesis: ( x in NAT \/ {+infty} implies b₁ in ExtREAL )
assume x in NAT \/ {+infty} ; :: thesis: b₁ in ExtREAL

per cases then ( x in NAT or x = +infty ) by ZFMISC_1:136;

suppose x in NAT ; :: thesis: b₁ in ExtREAL

then x in REAL by NUMBERS:19;
hence x in ExtREAL by NUMBERS:31; :: thesis: verum

end;

suppose x = +infty ; :: thesis: b₁ in ExtREAL

then x in {+infty,-infty} by TARSKI:def 2;
hence x in ExtREAL by XXREAL_0:def 4, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence NAT \/ {+infty} is Subset of ExtREAL by TARSKI:def 3; :: thesis: verum