let UN be non trivial Universe; :: thesis: ExtREAL * in UN
ExtREAL is Element of UN by Th54;
hence ExtREAL * in UN by Th64; :: thesis: verum