let n be object ; :: thesis: ( n is real implies n is ext-real )
assume n in REAL ; :: according to XREAL_0:def 1 :: thesis: n is ext-real
hence n in ExtREAL by XBOOLE_0:def 3; :: according to XXREAL_0:def 1 :: thesis: verum