let UN be non trivial Universe; :: thesis: ExtREAL is Element of UN
reconsider u = REAL as Element of UN by Th53;
0 is Element of UN by Th13;
then [0,u] is Element of UN by CLASSES2:3;
then {u,[0,u]} is Element of UN by CLASSES2:2;
hence ExtREAL is Element of UN by CLASSES2:60; :: thesis: verum