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

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