REAL in {REAL,[0,REAL]} by TARSKI:def 2;
then REAL in ExtREAL by XBOOLE_0:def 3;
hence REAL <> ExtREAL ; :: thesis: verum