take 0 ; :: thesis: 0 is ext-real
NAT c= ExtREAL by NUMBERS:19, NUMBERS:31;
hence 0 in ExtREAL ; :: according to XXREAL_0:def 1 :: thesis: verum