   Jensen’s consistency proof for TSTU (and thereby NFU) combines Ramsey theory with a technique that had been developed originally by Abraham Robinson [1939] to obtain a proof of the independence of extensionality from the other axioms of ZF.