# Re: [isabelle] [Isabelle] how to translate this into Isabelle language to prove the this

> Every poset is in which every chain has an upper bound has a maximal element => prove every vector space has a basis.
A straight forward translation (without thinking about what you might
want) to first order logic would be
lemma "â poset â {chain â Posets. â u. upper_bound u chain â is_max
u}. â vector_space. has_basis vector_space"
Note that you need to define Posets, upper_bound, is_max, and has_basis.
Also, note that the locally bound `poset` and `vector_space` are
completely independent. I guess the way I wrote it down, it is as hard
to show as
lemma "â vector_space. has_basis vector_space"
Probably you want to express that the vector_space is constructed
somehow with the poset.
Cornelius

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*