This is an unofficial reimagining of the Archive of Formal Proofs
Order Extension and Szpilrajn's Extension Theoremby Peter Zeller and Lukas Stevens