6.1202

⁡ x , etc. etc.

It is clear that we could have used for this purpose contradictions instead of tautologies.

544