La magia del lema de Zorn

Hace tiempo que me dijeron que todo espacio vectorial (de dimensión cualquiera) admite una base, y que para demostrarlo era necesario el Axioma de Elección (Axiom of Choice, AC) en el sentido de que si no añadiéramos este axioma a los axiomas de Zermelo-Fraenkel, existirían espacios vectoriales sin base, y claro, esto sería un auténtico desastre. Sin embargo hasta ahora no me había molestado en echar un vistazo a esta demostración, y como me ocurre casi siempre que veo una demostración que usa el AC, termino con la sensación de que la prueba se reduce a "lo hizo un mago".

La demostración no usa exactamente el AC, sino una caracterización suya: el lema de Zorn, que garantiza la existencia de elemento maximal para un conjunto pidiendo ciertas condiciones sobre una relación de orden definida en él. Ya que me he molestado en mirarlo, lo dejo aquí escrito a ver qué pensáis vosotros (en caso de que exista un "vosotros" porque sospecho que nadie me lee).