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