Thinking about the beauty of proofs, as imdicated by simplicity, and how breifly they can be encoded (information-theoretic version of occam's razor):
Another aspect of the symmetrical stackexchange diagram (two alternate interior angles), and Euclid's lop-sided one is that Euclid's is slightly simpler (one alternate interior angle, and one corresponding angle).
But from another perspective, the symmetrical one is simpler, because its symmetry allows it to be remembered as symmetry, and only recording one side.
Further, although stating it is symmetrical may require more information to record than just explicitly stating both sides if you only record one theorem, if you record a corpus of theorems and symmetry is common over that corpus (which it is), it can be stated with less information. (i.e, like using shorter words for frequently used concepts).
But this is only for the proof details; I'm not sure how it applies to the theorem as a reusable component, where you don't have to worry about the details.
Another aspect of the symmetrical stackexchange diagram (two alternate interior angles), and Euclid's lop-sided one is that Euclid's is slightly simpler (one alternate interior angle, and one corresponding angle).
But from another perspective, the symmetrical one is simpler, because its symmetry allows it to be remembered as symmetry, and only recording one side.
Further, although stating it is symmetrical may require more information to record than just explicitly stating both sides if you only record one theorem, if you record a corpus of theorems and symmetry is common over that corpus (which it is), it can be stated with less information. (i.e, like using shorter words for frequently used concepts).
But this is only for the proof details; I'm not sure how it applies to the theorem as a reusable component, where you don't have to worry about the details.