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