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: ExtNAT c< ExtREAL
-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

proof

assume -infty in ExtNAT ; :: thesis: contradiction

per cases then ( -infty in NAT or -infty in {+infty} ) by ZFMISC_1:136;

suppose -infty in NAT ; :: thesis: contradiction

hence contradiction ; :: thesis: verum

end;

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

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

end;

end;

end;

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