let x be object ; :: thesis:
assume x in NAT \/ {+infty} ; :: thesis:

per cases by ZFMISC_1:136;

suppose x in NAT ; :: thesis:

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

end;

suppose x = +infty ; :: thesis:

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

end;

end;

end;

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