  Now again the standard modeling in set theory gives us a problem: one can prove in ZF set theory that Tr has no solution whatsoever.  And this runs afoul of our pictures and intuition.  The standard way out is to change the equals sign = in (7) to something else.  For most mathematical work this is perfectly fine, but it is the kind of move we explore in this entry.