The sorted list example is neat! But the "formal" proof is still missing some steps. In particular, there's a key, unmentioned axiom that if a < b and b < c, then a < c. This is used in step 5, but not referenced explicitly. I think it would help to expand step 5 making this explicit.

This is nitpicking, of course, but making axioms explicit is part of formality. A fun aside could be pointing out that without transitivity, sorting lists with repeated elements may be possible! E.g., in the game of rock-paper-scissors, the list (rock, paper, scissors, rock) is perfectly sorted!