>>694
vectorの集合しか残っとらんやんけ。
大体、順序なんか関係ないのに列って何？
非可算基底の場合も含めて基底の存在証明したときも集合でやってたよなー。
Zornの補題を使ったから、基底集合間の包含順序を使ったけど。