REAL c< ExtREAL by Th31, Th32;