A2: +infty in ExtNAT by ZFMISC_1:136;
not +infty in NAT ;
hence NAT c< ExtNAT by A2, XBOOLE_1:7, XBOOLE_0:def 8; :: thesis:
-infty in {+infty,-infty} by TARSKI:def 2;
then A2: -infty in ExtREAL by XXREAL_0:def 4, XBOOLE_0:def 3;
not -infty in ExtNAT

assume -infty in ExtNAT ; :: thesis:

per cases by ZFMISC_1:136;

suppose -infty in NAT ; :: thesis:

hence contradiction ; :: thesis:

end;

suppose -infty in {+infty} ; :: thesis:

hence contradiction by TARSKI:def 1; :: thesis:

end;

end;

end;

hence ExtNAT c< ExtREAL by A2, XBOOLE_0:def 8; :: thesis: