https://www21.in.tum.de/team/stevensl
This is an unofficial reimagining of the Archive of Formal Proofs
Order Extension and Szpilrajn's Extension Theoremby Peter Zeller and Lukas Stevens