take 0 ; :: thesis: 0 is ext-real
thus 0 in ExtREAL by XBOOLE_0:def 3; :: according to XXREAL_0:def 1 :: thesis: verum